equal
deleted
inserted
replaced
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 if [ -x "$ML_HOME/polyimport" ]; then |
10 if [ -x "$ML_HOME/polyimport" ]; then |
11 "$ML_HOME/poly" -v | \ |
11 env LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \ |
|
12 "$ML_HOME/poly" -v | \ |
12 sed -n 's,^Poly/ML.*RTS version: [^ ]*\(-[^ ]*\).*$,\1,p' |
13 sed -n 's,^Poly/ML.*RTS version: [^ ]*\(-[^ ]*\).*$,\1,p' |
13 else |
14 else |
14 "$ML_HOME/poly" -noDisplay -r /dev/null | head -n 1 | \ |
15 "$ML_HOME/poly" -noDisplay -r /dev/null | head -n 1 | \ |
15 sed -n 's,^Poly/ML RTS version [^ ]*\(-[^ ]*\).*$,\1,p' |
16 sed -n 's,^Poly/ML RTS version [^ ]*\(-[^ ]*\).*$,\1,p' |
16 fi |
17 fi |