author | wenzelm |
Fri, 31 Oct 2014 22:09:18 +0100 | |
changeset 58855 | 2885e2eaa0fb |
parent 41515 | 2b456655b077 |
permissions | -rwxr-xr-x |
16996 | 1 |
#!/usr/bin/env bash |
2 |
# |
|
3 |
# polyml-version --- determine Poly/ML runtime system version |
|
4 |
||
41495 | 5 |
if [ -x "$ML_HOME/polyml-version" ]; then |
6 |
"$ML_HOME/polyml-version" |
|
7 |
elif [ -x "$ML_HOME/poly" ]; then |
|
40546
f46c902a8438
eliminated old-style sed in favour of builtin regex matching;
wenzelm
parents:
31695
diff
changeset
|
8 |
VERSION="$(env \ |
f46c902a8438
eliminated old-style sed in favour of builtin regex matching;
wenzelm
parents:
31695
diff
changeset
|
9 |
LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \ |
31695
36c5c15597f2
more robust poly startup, by restricting heap size (otherwise it fails on very large memory);
wenzelm
parents:
29145
diff
changeset
|
10 |
DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \ |
40546
f46c902a8438
eliminated old-style sed in favour of builtin regex matching;
wenzelm
parents:
31695
diff
changeset
|
11 |
"$ML_HOME/poly" -v -H 10)" |
f46c902a8438
eliminated old-style sed in favour of builtin regex matching;
wenzelm
parents:
31695
diff
changeset
|
12 |
REGEXP='^Poly/ML.*RTS version: [^ ]*(-[^ ]*).*$' |
f46c902a8438
eliminated old-style sed in favour of builtin regex matching;
wenzelm
parents:
31695
diff
changeset
|
13 |
if [[ "$VERSION" =~ $REGEXP ]]; then |
f46c902a8438
eliminated old-style sed in favour of builtin regex matching;
wenzelm
parents:
31695
diff
changeset
|
14 |
echo "polyml${BASH_REMATCH[1]}" |
f46c902a8438
eliminated old-style sed in favour of builtin regex matching;
wenzelm
parents:
31695
diff
changeset
|
15 |
else |
41515 | 16 |
echo polyml-undefined |
40546
f46c902a8438
eliminated old-style sed in favour of builtin regex matching;
wenzelm
parents:
31695
diff
changeset
|
17 |
fi |
f46c902a8438
eliminated old-style sed in favour of builtin regex matching;
wenzelm
parents:
31695
diff
changeset
|
18 |
else |
41515 | 19 |
echo polyml-undefined |
16996 | 20 |
fi |