isabelle: lib/scripts/polyml-version@92ddca1edc43 (annotated)

16996 32afaa947f6e determine Poly/ML runtime system version wenzelm parents: diff changeset	1	#!/usr/bin/env bash
32afaa947f6e determine Poly/ML runtime system version wenzelm parents: diff changeset	2	#
32afaa947f6e determine Poly/ML runtime system version wenzelm parents: diff changeset	3	# polyml-version --- determine Poly/ML runtime system version
32afaa947f6e determine Poly/ML runtime system version wenzelm parents: diff changeset	4
41495 f8c11067e124 updated for polyml-5.4.0; wenzelm parents: 40546 diff changeset	5	if [ -x "$ML_HOME/polyml-version" ]; then
f8c11067e124 updated for polyml-5.4.0; wenzelm parents: 40546 diff changeset	6	"$ML_HOME/polyml-version"
f8c11067e124 updated for polyml-5.4.0; wenzelm parents: 40546 diff changeset	7	elif [ -x "$ML_HOME/poly" ]; then
40546 f46c902a8438 eliminated old-style sed in favour of builtin regex matching; wenzelm parents: 31695 diff changeset	8	VERSION="$(env \
f46c902a8438 eliminated old-style sed in favour of builtin regex matching; wenzelm parents: 31695 diff changeset	9	LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \
31695 36c5c15597f2 more robust poly startup, by restricting heap size (otherwise it fails on very large memory); wenzelm parents: 29145 diff changeset	10	DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \
40546 f46c902a8438 eliminated old-style sed in favour of builtin regex matching; wenzelm parents: 31695 diff changeset	11	"$ML_HOME/poly" -v -H 10)"
f46c902a8438 eliminated old-style sed in favour of builtin regex matching; wenzelm parents: 31695 diff changeset	12	REGEXP='^Poly/ML.RTS version: [^ ](-[^ ]).$'
f46c902a8438 eliminated old-style sed in favour of builtin regex matching; wenzelm parents: 31695 diff changeset	13	if [[ "$VERSION" =~ $REGEXP ]]; then
f46c902a8438 eliminated old-style sed in favour of builtin regex matching; wenzelm parents: 31695 diff changeset	14	echo "polyml${BASH_REMATCH[1]}"
f46c902a8438 eliminated old-style sed in favour of builtin regex matching; wenzelm parents: 31695 diff changeset	15	else
41515 2b456655b077 tuned (cf. 2fe62d602681); wenzelm parents: 41495 diff changeset	16	echo polyml-undefined
40546 f46c902a8438 eliminated old-style sed in favour of builtin regex matching; wenzelm parents: 31695 diff changeset	17	fi
f46c902a8438 eliminated old-style sed in favour of builtin regex matching; wenzelm parents: 31695 diff changeset	18	else
41515 2b456655b077 tuned (cf. 2fe62d602681); wenzelm parents: 41495 diff changeset	19	echo polyml-undefined
16996 32afaa947f6e determine Poly/ML runtime system version wenzelm parents: diff changeset	20	fi

author	paulson
	Thu, 14 Jun 2018 14:23:48 +0100
changeset 68446	92ddca1edc43
parent 41515	2b456655b077
permissions	-rwxr-xr-x