# HG changeset patch
# User wenzelm
# Date 1308772475 -7200
# Node ID 55160cf1e4f658bad962492af4c2932fa98961ce
# Parent  45cf8d5e109a9e494adeccf0fba2a29f60f167d1
clarified default ML settings;

diff -r 45cf8d5e109a -r 55160cf1e4f6 etc/settings
--- a/etc/settings	Wed Jun 22 21:35:48 2011 +0200
+++ b/etc/settings	Wed Jun 22 21:54:35 2011 +0200
@@ -15,7 +15,7 @@
 # not invent new ML system names unless you know what you are doing.
 # Only one of the sections below should be activated.
 
-# Poly/ML 5.x (automated settings)
+# Poly/ML 32 bit (automated settings)
 ML_PLATFORM="$ISABELLE_PLATFORM"
 ML_HOME="$(choosefrom \
   "$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM" \
@@ -28,17 +28,17 @@
 ML_OPTIONS="-H 200"
 ML_SOURCES="$ML_HOME/../src"
 
-# Poly/ML 5.4.0
-#ML_PLATFORM=x86-linux
-#ML_HOME=/usr/local/polyml/x86-linux
+# Poly/ML 32 bit (manual settings)
 #ML_SYSTEM=polyml-5.4.0
+#ML_PLATFORM="$ISABELLE_PLATFORM"
+#ML_HOME="$ISABELLE_HOME/contrib/$ML_SYSTEM/$ML_PLATFORM"
 #ML_OPTIONS="-H 500"
 #ML_SOURCES="$ML_HOME/../src"
 
-# Poly/ML 5.4.0 (64 bit)
-#ML_PLATFORM=x86_64-linux
-#ML_HOME=/usr/local/polyml/x86_64-linux
+# Poly/ML 64 bit (manual settings)
 #ML_SYSTEM=polyml-5.4.0
+#ML_PLATFORM="${ISABELLE_PLATFORM64:-$ISABELLE_PLATFORM}"
+#ML_HOME="$ISABELLE_HOME/contrib/$ML_SYSTEM/$ML_PLATFORM"
 #ML_OPTIONS="-H 1000"
 #ML_SOURCES="$ML_HOME/../src"