diff -r 364f672d8827 -r f8c11067e124 lib/scripts/polyml-version --- 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" \