1#!/usr/bin/env bash 2# 3# polyml-version --- determine Poly/ML runtime system version 4 5if [ -x "$ML_HOME/polyml-version" ]; then 6 "$ML_HOME/polyml-version" 7elif [ -x "$ML_HOME/poly" ]; then 8 VERSION="$(env \ 9 LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \ 10 DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \ 11 "$ML_HOME/poly" -v -H 10)" 12 REGEXP='^Poly/ML.*RTS version: [^ ]*(-[^ ]*).*$' 13 if [[ "$VERSION" =~ $REGEXP ]]; then 14 echo "polyml${BASH_REMATCH[1]}" 15 else 16 echo polyml-undefined 17 fi 18else 19 echo polyml-undefined 20fi 21