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 if [ -x "$ML_HOME/poly" ]; then |
5 if [ -x "$ML_HOME/polyml-version" ]; then |
|
6 "$ML_HOME/polyml-version" |
|
7 elif [ -x "$ML_HOME/poly" ]; then |
6 VERSION="$(env \ |
8 VERSION="$(env \ |
7 LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \ |
9 LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \ |
8 DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \ |
10 DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \ |
9 "$ML_HOME/poly" -v -H 10)" |
11 "$ML_HOME/poly" -v -H 10)" |
10 REGEXP='^Poly/ML.*RTS version: [^ ]*(-[^ ]*).*$' |
12 REGEXP='^Poly/ML.*RTS version: [^ ]*(-[^ ]*).*$' |