lib/scripts/polyml-version
author wenzelm
Sat Dec 20 11:55:34 2008 +0100 (2008-12-20)
changeset 29145 b1c6f4563df7
parent 21652 3501b5a8a2c1
child 31695 36c5c15597f2
permissions -rwxr-xr-x
removed Ids;
     1 #!/usr/bin/env bash
     2 #
     3 # polyml-version --- determine Poly/ML runtime system version
     4 
     5 echo -n polyml
     6 
     7 if [ -x "$ML_HOME/poly" ]; then
     8   if [ -x "$ML_HOME/polyimport" ]; then
     9     env LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \
    10       DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \
    11       "$ML_HOME/poly" -v | \
    12       sed -n 's,^Poly/ML.*RTS version: [^ ]*\(-[^ ]*\).*$,\1,p'
    13   else
    14     "$ML_HOME/poly" -noDisplay -r /dev/null | head -n 1 | \
    15       sed -n 's,^Poly/ML RTS version [^ ]*\(-[^ ]*\).*$,\1,p'
    16   fi
    17 fi