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