| author | wenzelm |
| Sat, 20 Dec 2008 11:55:34 +0100 | |
| changeset 29145 | b1c6f4563df7 |
| parent 21652 | 3501b5a8a2c1 |
| child 31695 | 36c5c15597f2 |
| permissions | -rwxr-xr-x |
1 #!/usr/bin/env bash
2 #
3 # polyml-version --- determine Poly/ML runtime system version
5 echo -n polyml
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