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