author  wenzelm 
Fri, 16 Apr 2010 10:52:10 +0200  
changeset 36162  0bd034a80a9a 
parent 31695  36c5c15597f2 
child 40546  f46c902a8438 
permissions  rwxrxrx 
16996  1 
#!/usr/bin/env bash 
2 
# 

3 
# polymlversion  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 