lib/scripts/polyml-version
changeset 17419 16df5a5eef68
parent 16996 32afaa947f6e
child 20748 4bcf492c6c9d
equal deleted inserted replaced
17418:cd5d8b444d6e 17419:16df5a5eef68
     5 # polyml-version --- determine Poly/ML runtime system version
     5 # polyml-version --- determine Poly/ML runtime system version
     6 
     6 
     7 echo -n polyml
     7 echo -n polyml
     8 
     8 
     9 if [ -x "$ML_HOME/poly" ]; then
     9 if [ -x "$ML_HOME/poly" ]; then
    10   "$ML_HOME/poly" -r /dev/null | head -n 1 | \
    10   "$ML_HOME/poly" -noDisplay -r /dev/null | head -n 1 | \
    11     sed -n 's,^Poly/ML RTS version [^ ]*\(-[^ ]*\).*$,\1,p'
    11     sed -n 's,^Poly/ML RTS version [^ ]*\(-[^ ]*\).*$,\1,p'
    12 fi
    12 fi