isabelle: lib/scripts/polyml-version@52dc576f1759 (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	echo -n polyml
32afaa947f6e determine Poly/ML runtime system version wenzelm parents: diff changeset	6
32afaa947f6e determine Poly/ML runtime system version wenzelm parents: diff changeset	7	if [ -x "$ML_HOME/poly" ]; then
31695 36c5c15597f2 more robust poly startup, by restricting heap size (otherwise it fails on very large memory); wenzelm parents: 29145 diff changeset	8	env LD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$LD_LIBRARY_PATH" \
36c5c15597f2 more robust poly startup, by restricting heap size (otherwise it fails on very large memory); wenzelm parents: 29145 diff changeset	9	DYLD_LIBRARY_PATH="$ML_HOME:$ML_HOME/../lib:$DYLD_LIBRARY_PATH" \
36c5c15597f2 more robust poly startup, by restricting heap size (otherwise it fails on very large memory); wenzelm parents: 29145 diff changeset	10	"$ML_HOME/poly" -v -H 10 \| \
36c5c15597f2 more robust poly startup, by restricting heap size (otherwise it fails on very large memory); wenzelm parents: 29145 diff changeset	11	sed -n 's,^Poly/ML.RTS version: [^ ]$-[^ ]$.$,\1,p'
16996 32afaa947f6e determine Poly/ML runtime system version wenzelm parents: diff changeset	12	fi

author	krauss
	Fri, 04 Jun 2010 16:02:46 +0200
changeset 37316	52dc576f1759
parent 31695	36c5c15597f2
child 40546	f46c902a8438
permissions	-rwxr-xr-x