--- a/lib/scripts/polyml-version Mon Nov 15 17:14:43 2010 +0100
+++ b/lib/scripts/polyml-version Mon Nov 15 17:39:23 2010 +0100
@@ -2,11 +2,17 @@
#
# polyml-version --- determine Poly/ML runtime system version
-echo -n polyml
-
if [ -x "$ML_HOME/poly" ]; then
- env LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \
+ VERSION="$(env \
+ LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \
DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \
- "$ML_HOME/poly" -v -H 10 | \
- sed -n 's,^Poly/ML.*RTS version: [^ ]*\(-[^ ]*\).*$,\1,p'
+ "$ML_HOME/poly" -v -H 10)"
+ REGEXP='^Poly/ML.*RTS version: [^ ]*(-[^ ]*).*$'
+ if [[ "$VERSION" =~ $REGEXP ]]; then
+ echo "polyml${BASH_REMATCH[1]}"
+ else
+ echo polyml-unknown
+ fi
+else
+ echo polyml-unknown
fi