tuned (cf. 2fe62d602681);
authorwenzelm
Tue Jan 11 21:52:10 2011 +0100 (2011-01-11)
changeset 415152b456655b077
parent 41514 917f1a4fbc77
child 41516 3a70387b5e01
tuned (cf. 2fe62d602681);
lib/scripts/polyml-version
     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