equal
deleted
inserted
replaced
1 #!/usr/bin/env bash |
1 #!/usr/bin/env bash |
2 # |
2 # |
3 # polyml-version --- determine Poly/ML runtime system version |
3 # polyml-version --- determine Poly/ML runtime system version |
4 |
4 |
5 echo -n polyml |
|
6 |
|
7 if [ -x "$ML_HOME/poly" ]; then |
5 if [ -x "$ML_HOME/poly" ]; then |
8 env LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \ |
6 VERSION="$(env \ |
|
7 LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \ |
9 DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \ |
8 DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \ |
10 "$ML_HOME/poly" -v -H 10 | \ |
9 "$ML_HOME/poly" -v -H 10)" |
11 sed -n 's,^Poly/ML.*RTS version: [^ ]*\(-[^ ]*\).*$,\1,p' |
10 REGEXP='^Poly/ML.*RTS version: [^ ]*(-[^ ]*).*$' |
|
11 if [[ "$VERSION" =~ $REGEXP ]]; then |
|
12 echo "polyml${BASH_REMATCH[1]}" |
|
13 else |
|
14 echo polyml-unknown |
|
15 fi |
|
16 else |
|
17 echo polyml-unknown |
12 fi |
18 fi |