lib/scripts/polyml-version
changeset 41515 2b456655b077
parent 41495 f8c11067e124
--- 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