# HG changeset patch
# User wenzelm
# Date 1243772192 -7200
# Node ID be0c4236fe44433539c7c0c2249d3efc2d66e274
# Parent  3fd52453ae8141fa42a768d2545cfb75e46a38ac
updated example settings;

diff -r 3fd52453ae81 -r be0c4236fe44 etc/settings
--- a/etc/settings	Sun May 31 14:15:07 2009 +0200
+++ b/etc/settings	Sun May 31 14:16:32 2009 +0200
@@ -29,16 +29,16 @@
 ML_OPTIONS="-H 200"
 ML_DBASE=""
 
-# Poly/ML 5.1
+# Poly/ML 5.2.1
 #ML_PLATFORM=x86-linux
 #ML_HOME=/usr/local/polyml/x86-linux
-#ML_SYSTEM=polyml-5.1
+#ML_SYSTEM=polyml-5.2.1
 #ML_OPTIONS="-H 500"
 
-# Poly/ML 5.1 (64 bit)
+# Poly/ML 5.2.1 (64 bit)
 #ML_PLATFORM=x86_64-linux
 #ML_HOME=/usr/local/polyml/x86_64-linux
-#ML_SYSTEM=polyml-5.1
+#ML_SYSTEM=polyml-5.2.1
 #ML_OPTIONS="-H 1000"
 
 # Standard ML of New Jersey (slow!)