updated to jedit_build-20181025 according to patches/macos (Java 11), patches/putenv;
proper update of jEdit environment -- avoid warnings in Java 11;
activate jdk-11+28;
#!/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