| author | wenzelm |
| Fri, 16 Apr 2010 22:52:49 +0200 | |
| changeset 36180 | 2db3711b2b03 |
| 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 |