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