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" \