--- 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