lib/scripts/polyml-version
author wenzelm
Wed Sep 27 23:41:12 2006 +0200 (2006-09-27)
changeset 20748 4bcf492c6c9d
parent 17419 16df5a5eef68
child 20758 19be439e35f9
permissions -rwxr-xr-x
adapted to pre-5.0 versions;
wenzelm@16996
     1
#!/usr/bin/env bash
wenzelm@16996
     2
#
wenzelm@16996
     3
# $Id$
wenzelm@16996
     4
#
wenzelm@16996
     5
# polyml-version --- determine Poly/ML runtime system version
wenzelm@16996
     6
wenzelm@16996
     7
echo -n polyml
wenzelm@16996
     8
wenzelm@16996
     9
if [ -x "$ML_HOME/poly" ]; then
wenzelm@20748
    10
  if [ -x "$ML_HOME/polyimport" ]; then
wenzelm@20748
    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