# HG changeset patch
# User wenzelm
# Date 1129905262 -7200
# Node ID 42fc2ac69c8cfbc3b4031436b956a2bf52569b9d
# Parent  b74eb797b6c2ed72d2b799fdb7ceaca4ff8cb64b
added simplified settings for Poly/ML 4.x (commented out);

diff -r b74eb797b6c2 -r 42fc2ac69c8c etc/settings
--- a/etc/settings	Fri Oct 21 16:22:59 2005 +0200
+++ b/etc/settings	Fri Oct 21 16:34:22 2005 +0200
@@ -16,7 +16,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 4.x
+# Poly/ML 4.x (automated settings)
 POLY_HOME="$(type -p poly)"; [ -n "$POLY_HOME" ] && POLY_HOME="$(dirname "$POLY_HOME")"
 ML_PLATFORM=$("$ISABELLE_HOME/lib/scripts/polyml-platform")
 ML_HOME=$(choosefrom \
@@ -30,6 +30,12 @@
 ML_OPTIONS="-H 80"
 ML_DBASE=""
 
+# Poly/ML 4.x
+#ML_PLATFORM=$("$ISABELLE_HOME/lib/scripts/polyml-platform")
+#ML_HOME="$ISABELLE_HOME/contrib/polyml/$ML_PLATFORM/$ML_PLATFORM"
+#ML_SYSTEM=$("$ISABELLE_HOME/lib/scripts/polyml-version")
+#ML_OPTIONS="-H 80"
+
 # Standard ML of New Jersey 110 or later
 #SMLNJ_CYGWIN_RUNTIME=1
 #ML_SYSTEM=smlnj-110