lib/scripts/polyml-version
changeset 41495 f8c11067e124
parent 40546 f46c902a8438
child 41515 2b456655b077
--- a/lib/scripts/polyml-version	Mon Jan 10 16:56:47 2011 +0100
+++ b/lib/scripts/polyml-version	Mon Jan 10 17:22:48 2011 +0100
@@ -2,7 +2,9 @@
 #
 # polyml-version --- determine Poly/ML runtime system version
 
-if [ -x "$ML_HOME/poly" ]; then
+if [ -x "$ML_HOME/polyml-version" ]; then
+  "$ML_HOME/polyml-version"
+elif [ -x "$ML_HOME/poly" ]; then
   VERSION="$(env \
     LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \
     DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \