diff -r 1082f0d6628b -r 1e10689ee184 lib/scripts/polyml-version
--- a/lib/scripts/polyml-version	Thu Mar 02 15:39:21 2023 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,20 +0,0 @@
-#!/usr/bin/env bash
-#
-# polyml-version --- determine Poly/ML runtime system version
-
-if [ -x "$ML_HOME/polyml-version" ]; then
-  "$ML_HOME/polyml-version"
-elif [ -x "$ML_HOME/poly" ]; then
-  VERSION="$(env \
-    LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \
-    DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \
-    "$ML_HOME/poly" -v -H 10)"
-  REGEXP='^Poly/ML.*RTS version: [^ ]*(-[^ ]*).*$'
-  if [[ "$VERSION" =~ $REGEXP ]]; then
-    echo "polyml${BASH_REMATCH[1]}"
-  else
-    echo polyml-undefined
-  fi
-else
-  echo polyml-undefined
-fi