isabelle: lib/scripts/polyml-version@390c53904220 (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
32afaa947f6e determine Poly/ML runtime system version wenzelm parents: diff changeset	5	if [ -x "$ML_HOME/poly" ]; then
40546 f46c902a8438 eliminated old-style sed in favour of builtin regex matching; wenzelm parents: 31695 diff changeset	6	VERSION="$(env \
f46c902a8438 eliminated old-style sed in favour of builtin regex matching; wenzelm parents: 31695 diff changeset	7	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	8	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	9	"$ML_HOME/poly" -v -H 10)"
f46c902a8438 eliminated old-style sed in favour of builtin regex matching; wenzelm parents: 31695 diff changeset	10	REGEXP='^Poly/ML.RTS version: [^ ](-[^ ]).$'
f46c902a8438 eliminated old-style sed in favour of builtin regex matching; wenzelm parents: 31695 diff changeset	11	if [[ "$VERSION" =~ $REGEXP ]]; then
f46c902a8438 eliminated old-style sed in favour of builtin regex matching; wenzelm parents: 31695 diff changeset	12	echo "polyml${BASH_REMATCH[1]}"
f46c902a8438 eliminated old-style sed in favour of builtin regex matching; wenzelm parents: 31695 diff changeset	13	else
f46c902a8438 eliminated old-style sed in favour of builtin regex matching; wenzelm parents: 31695 diff changeset	14	echo polyml-unknown
f46c902a8438 eliminated old-style sed in favour of builtin regex matching; wenzelm parents: 31695 diff changeset	15	fi
f46c902a8438 eliminated old-style sed in favour of builtin regex matching; wenzelm parents: 31695 diff changeset	16	else
f46c902a8438 eliminated old-style sed in favour of builtin regex matching; wenzelm parents: 31695 diff changeset	17	echo polyml-unknown
16996 32afaa947f6e determine Poly/ML runtime system version wenzelm parents: diff changeset	18	fi

author	wenzelm
	Tue, 21 Dec 2010 21:21:21 +0100
changeset 41377	390c53904220
parent 40546	f46c902a8438
child 41495	f8c11067e124
permissions	-rwxr-xr-x