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