author | wenzelm |
Tue, 11 Jan 2011 21:52:10 +0100 | |
changeset 41515 | 2b456655b077 |
parent 41514 | 917f1a4fbc77 |
child 41516 | 3a70387b5e01 |
--- 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