| changeset 41515 | 2b456655b077 |
| parent 41495 | f8c11067e124 |
| 41514:917f1a4fbc77 | 41515:2b456655b077 |
|---|---|
11 "$ML_HOME/poly" -v -H 10)" |
11 "$ML_HOME/poly" -v -H 10)" |
12 REGEXP='^Poly/ML.*RTS version: [^ ]*(-[^ ]*).*$' |
12 REGEXP='^Poly/ML.*RTS version: [^ ]*(-[^ ]*).*$' |
13 if [[ "$VERSION" =~ $REGEXP ]]; then |
13 if [[ "$VERSION" =~ $REGEXP ]]; then |
14 echo "polyml${BASH_REMATCH[1]}" |
14 echo "polyml${BASH_REMATCH[1]}" |
15 else |
15 else |
16 echo polyml-unknown |
16 echo polyml-undefined |
17 fi |
17 fi |
18 else |
18 else |
19 echo polyml-unknown |
19 echo polyml-undefined |
20 fi |
20 fi |