# HG changeset patch
# User wenzelm
# Date 1139534533 -3600
# Node ID 61c7875a58b81cc120f040aeacd01425dc204ccc
# Parent  5060ca625e020193efd02922804af07349c2f4d6
simplified polyml example;

diff -r 5060ca625e02 -r 61c7875a58b8 etc/settings
--- a/etc/settings	Thu Feb 09 12:20:31 2006 +0100
+++ b/etc/settings	Fri Feb 10 02:22:13 2006 +0100
@@ -30,10 +30,10 @@
 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")
+# Poly/ML 4.2.0 (manual settings)
+#ML_PLATFORM=x86-linux
+#ML_HOME=/usr/local/polyml/x86-linux"
+#ML_SYSTEM=polyml-4.2.0
 #ML_OPTIONS="-H 80"
 
 # Standard ML of New Jersey 110 or later