|
16996
|
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
|
|
17419
|
10 |
"$ML_HOME/poly" -noDisplay -r /dev/null | head -n 1 | \
|
|
16996
|
11 |
sed -n 's,^Poly/ML RTS version [^ ]*\(-[^ ]*\).*$,\1,p'
|
|
|
12 |
fi
|