| changeset 16996 | 32afaa947f6e |
| child 17419 | 16df5a5eef68 |
| 16995:5b344d1dccd8 | 16996:32afaa947f6e |
|---|---|
1 #!/usr/bin/env bash |
|
2 # |
|
3 # $Id$ |
|
4 # |
|
5 # polyml-version --- determine Poly/ML runtime system version |
|
6 |
|
7 echo -n polyml |
|
8 |
|
9 if [ -x "$ML_HOME/poly" ]; then |
|
10 "$ML_HOME/poly" -r /dev/null | head -n 1 | \ |
|
11 sed -n 's,^Poly/ML RTS version [^ ]*\(-[^ ]*\).*$,\1,p' |
|
12 fi |