| author | wenzelm |
| Thu, 28 Sep 2006 11:55:56 +0200 | |
| changeset 20758 | 19be439e35f9 |
| parent 20748 | 4bcf492c6c9d |
| child 21652 | 3501b5a8a2c1 |
| permissions | -rwxr-xr-x |
1 #!/usr/bin/env bash
2 #
3 # $Id$
4 #
5 # polyml-version --- determine Poly/ML runtime system version
7 echo -n polyml
9 if [ -x "$ML_HOME/poly" ]; then
10 if [ -x "$ML_HOME/polyimport" ]; then
11 env LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \
12 "$ML_HOME/poly" -v | \
13 sed -n 's,^Poly/ML.*RTS version: [^ ]*\(-[^ ]*\).*$,\1,p'
14 else
15 "$ML_HOME/poly" -noDisplay -r /dev/null | head -n 1 | \
16 sed -n 's,^Poly/ML RTS version [^ ]*\(-[^ ]*\).*$,\1,p'
17 fi
18 fi