etc/settings
changeset 20764 4aa5c89b933e
parent 20033 2b8dbb637792
child 20987 d1674119d0f9
--- 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