diff -r 052b348a98a9 -r 4aa5c89b933e etc/settings
--- a/etc/settings	Thu Sep 28 19:04:13 2006 +0200
+++ b/etc/settings	Thu Sep 28 20:30:53 2006 +0200
@@ -36,6 +36,12 @@
 #ML_SYSTEM=polyml-4.2.0
 #ML_OPTIONS="-H 80"
 
+# Poly/ML 4.9.1 (experimental!)
+#ML_PLATFORM=x86_64-linux
+#ML_HOME=/usr/local/polyml/x86_64-linux
+#ML_SYSTEM=polyml-4.9.1
+#ML_OPTIONS="-H 160"
+
 # Standard ML of New Jersey 110 or later
 #SMLNJ_CYGWIN_RUNTIME=1
 #ML_SYSTEM=smlnj-110