etc/settings
changeset 17825 ede984daba01
parent 17793 017e57b1f4d0
child 17905 1574533861b1
--- a/etc/settings	Tue Oct 11 13:28:08 2005 +0200
+++ b/etc/settings	Tue Oct 11 13:30:17 2005 +0200
@@ -40,15 +40,15 @@
 # Moscow ML 2.00 or later (experimental!)
 #ML_SYSTEM=mosml
 #ML_HOME="$ISABELLE_HOME/contrib/mosml/bin"
+#ML_OPTIONS=""
 #ML_PLATFORM=""
-#ML_OPTIONS=""
 
 # Poplog/PML version 15.6/2.1 (experimental!)
 #ML_SYSTEM=poplogml
-#ML_HOME="$ISABELLE_HOME/contrib/poplog/current-poplog/bin"
-#ML_PLATFORM=""
+#ML_HOME="/usr/local/poplog/current-poplog/bin"
 #ML_OPTIONS="-noinit"
 #ML_SUFFIX=".psv"
+#ML_PLATFORM=""
 
 
 ###