# HG changeset patch
# User wenzelm
# Date 1294676568 -3600
# Node ID f8c11067e124e77eddff5540d621651662fbe680
# Parent  364f672d88279a24773d31160a7f461204b9ebde
updated for polyml-5.4.0;
discontinued old-fashioned POLY_HOME via path;
more robust handling of polyml-version, preferably provided by Poly/ML distribution itself;

diff -r 364f672d8827 -r f8c11067e124 etc/settings
--- a/etc/settings	Mon Jan 10 16:56:47 2011 +0100
+++ b/etc/settings	Mon Jan 10 17:22:48 2011 +0100
@@ -16,7 +16,6 @@
 # Only one of the sections below should be activated.
 
 # Poly/ML 5.x (automated settings)
-POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$(dirname "$POLY_HOME")"
 ML_PLATFORM="$ISABELLE_PLATFORM"
 ML_HOME="$(choosefrom \
   "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \
@@ -24,22 +23,22 @@
   "/usr/local/polyml/$ML_PLATFORM" \
   "/usr/share/polyml/$ML_PLATFORM" \
   "/opt/polyml/$ML_PLATFORM" \
-  "$POLY_HOME")"
+  "")"
 ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
 ML_OPTIONS="-H 200"
 ML_SOURCES="$ML_HOME/../src"
 
-# Poly/ML 5.3.0
+# Poly/ML 5.4.0
 #ML_PLATFORM=x86-linux
 #ML_HOME=/usr/local/polyml/x86-linux
-#ML_SYSTEM=polyml-5.3.0
+#ML_SYSTEM=polyml-5.4.0
 #ML_OPTIONS="-H 500"
 #ML_SOURCES="$ML_HOME/../src"
 
-# Poly/ML 5.3.0 (64 bit)
+# Poly/ML 5.4.0 (64 bit)
 #ML_PLATFORM=x86_64-linux
 #ML_HOME=/usr/local/polyml/x86_64-linux
-#ML_SYSTEM=polyml-5.3.0
+#ML_SYSTEM=polyml-5.4.0
 #ML_OPTIONS="-H 1000"
 #ML_SOURCES="$ML_HOME/../src"
 
diff -r 364f672d8827 -r f8c11067e124 lib/scripts/polyml-version
--- a/lib/scripts/polyml-version	Mon Jan 10 16:56:47 2011 +0100
+++ b/lib/scripts/polyml-version	Mon Jan 10 17:22:48 2011 +0100
@@ -2,7 +2,9 @@
 #
 # polyml-version --- determine Poly/ML runtime system version
 
-if [ -x "$ML_HOME/poly" ]; then
+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" \