lib/scripts/polyml-version
changeset 41515 2b456655b077
parent 41495 f8c11067e124
     1.1 --- a/lib/scripts/polyml-version	Tue Jan 11 20:18:48 2011 +0100
     1.2 +++ b/lib/scripts/polyml-version	Tue Jan 11 21:52:10 2011 +0100
     1.3 @@ -13,8 +13,8 @@
     1.4    if [[ "$VERSION" =~ $REGEXP ]]; then
     1.5      echo "polyml${BASH_REMATCH[1]}"
     1.6    else
     1.7 -    echo polyml-unknown
     1.8 +    echo polyml-undefined
     1.9    fi
    1.10  else
    1.11 -  echo polyml-unknown
    1.12 +  echo polyml-undefined
    1.13  fi