diff -r 3501b5a8a2c1 -r 219924615db6 etc/settings
--- a/etc/settings	Tue Dec 05 18:32:54 2006 +0100
+++ b/etc/settings	Tue Dec 05 18:33:29 2006 +0100
@@ -36,10 +36,10 @@
 #ML_SYSTEM=polyml-4.2.0
 #ML_OPTIONS="-H 80"
 
-# Poly/ML 4.9.1 (experimental!)
+# Poly/ML 5.0
 #ML_PLATFORM=x86_64-linux
 #ML_HOME=/usr/local/polyml/x86_64-linux
-#ML_SYSTEM=polyml-4.9.1
+#ML_SYSTEM=polyml-5.0
 #ML_OPTIONS="-H 500"
 
 # Standard ML of New Jersey 110 or later