author | wenzelm |
Mon, 01 Aug 2005 19:20:49 +0200 | |
changeset 16996 | 32afaa947f6e |
parent 16995 | 5b344d1dccd8 |
child 16997 | 7dfc99f62dd9 |
--- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/lib/scripts/polyml-version Mon Aug 01 19:20:49 2005 +0200 @@ -0,0 +1,12 @@ +#!/usr/bin/env bash +# +# $Id$ +# +# polyml-version --- determine Poly/ML runtime system version + +echo -n polyml + +if [ -x "$ML_HOME/poly" ]; then + "$ML_HOME/poly" -r /dev/null | head -n 1 | \ + sed -n 's,^Poly/ML RTS version [^ ]*\(-[^ ]*\).*$,\1,p' +fi