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;
wenzelm@16996
     1
#!/usr/bin/env bash
wenzelm@16996
     2
#
wenzelm@16996
     3
# polyml-version --- determine Poly/ML runtime system version
wenzelm@16996
     4
wenzelm@16996
     5
echo -n polyml
wenzelm@16996
     6
wenzelm@16996
     7
if [ -x "$ML_HOME/poly" ]; then
wenzelm@20748
     8
  if [ -x "$ML_HOME/polyimport" ]; then
wenzelm@20758
     9
    env LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \
wenzelm@21652
    10
      DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \
wenzelm@20758
    11
      "$ML_HOME/poly" -v | \
wenzelm@20748
    12
      sed -n 's,^Poly/ML.*RTS version: [^ ]*\(-[^ ]*\).*$,\1,p'
wenzelm@20748
    13
  else
wenzelm@20748
    14
    "$ML_HOME/poly" -noDisplay -r /dev/null | head -n 1 | \
wenzelm@20748
    15
      sed -n 's,^Poly/ML RTS version [^ ]*\(-[^ ]*\).*$,\1,p'
wenzelm@20748
    16
  fi
wenzelm@16996
    17
fi