diff -r 917f1a4fbc77 -r 2b456655b077 lib/scripts/polyml-version --- a/lib/scripts/polyml-version Tue Jan 11 20:18:48 2011 +0100 +++ b/lib/scripts/polyml-version Tue Jan 11 21:52:10 2011 +0100 @@ -13,8 +13,8 @@ if [[ "$VERSION" =~ $REGEXP ]]; then echo "polyml${BASH_REMATCH[1]}" else - echo polyml-unknown + echo polyml-undefined fi else - echo polyml-unknown + echo polyml-undefined fi