| author | paulson |
| Tue, 02 Feb 2010 09:48:20 +0000 | |
| changeset 35503 | 7bba12c3b7b6 |
| parent 31695 | 36c5c15597f2 |
| child 40546 | f46c902a8438 |
| permissions | -rwxr-xr-x |
| 16996 | 1 |
#!/usr/bin/env bash |
2 |
# |
|
3 |
# polyml-version --- determine Poly/ML runtime system version |
|
4 |
||
5 |
echo -n polyml |
|
6 |
||
7 |
if [ -x "$ML_HOME/poly" ]; then |
|
|
31695
36c5c15597f2
more robust poly startup, by restricting heap size (otherwise it fails on very large memory);
wenzelm
parents:
29145
diff
changeset
|
8 |
env LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \ |
|
36c5c15597f2
more robust poly startup, by restricting heap size (otherwise it fails on very large memory);
wenzelm
parents:
29145
diff
changeset
|
9 |
DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \ |
|
36c5c15597f2
more robust poly startup, by restricting heap size (otherwise it fails on very large memory);
wenzelm
parents:
29145
diff
changeset
|
10 |
"$ML_HOME/poly" -v -H 10 | \ |
|
36c5c15597f2
more robust poly startup, by restricting heap size (otherwise it fails on very large memory);
wenzelm
parents:
29145
diff
changeset
|
11 |
sed -n 's,^Poly/ML.*RTS version: [^ ]*\(-[^ ]*\).*$,\1,p' |
| 16996 | 12 |
fi |