diff -r 5b344d1dccd8 -r 32afaa947f6e lib/scripts/polyml-version
--- /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