diff -r c23663825e23 -r 4fa98c1df7ba etc/settings
--- a/etc/settings	Thu Jun 04 22:52:53 2009 +0200
+++ b/etc/settings	Thu Jun 04 23:42:11 2009 +0200
@@ -41,6 +41,13 @@
 #ML_SYSTEM=polyml-5.2.1
 #ML_OPTIONS="-H 1000"
 
+# Poly/ML 5.3 (experimental)
+#ML_PLATFORM=x86-linux
+#ML_HOME=/usr/local/polyml/x86-linux
+#ML_SYSTEM=polyml-experimental
+#ML_OPTIONS="-H 500"
+#ML_SOURCES="$ML_HOME/../src"
+
 # Standard ML of New Jersey (slow!)
 #ML_SYSTEM=smlnj-110
 #ML_HOME="/usr/local/smlnj/bin"