equal
deleted
inserted
replaced
3 # polyml-version --- determine Poly/ML runtime system version |
3 # polyml-version --- determine Poly/ML runtime system version |
4 |
4 |
5 echo -n polyml |
5 echo -n polyml |
6 |
6 |
7 if [ -x "$ML_HOME/poly" ]; then |
7 if [ -x "$ML_HOME/poly" ]; then |
8 if [ -x "$ML_HOME/polyimport" ]; then |
8 env LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \ |
9 env LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \ |
9 DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \ |
10 DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \ |
10 "$ML_HOME/poly" -v -H 10 | \ |
11 "$ML_HOME/poly" -v | \ |
11 sed -n 's,^Poly/ML.*RTS version: [^ ]*\(-[^ ]*\).*$,\1,p' |
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 |
|
17 fi |
12 fi |