diff -r bd57acd44fc1 -r 83060e826e02 etc/settings --- a/etc/settings Wed Jul 05 18:27:55 2000 +0200 +++ b/etc/settings Thu Jul 06 00:08:24 2000 +0200 @@ -27,16 +27,16 @@ #ML_OPTIONS="@SMLdebug=/dev/null" #ML_PLATFORM=$(eval $($ML_HOME/.arch-n-opsys 2>/dev/null); echo $HEAP_SUFFIX) -# MLWorks 2.0 or later -#ML_SYSTEM=mlworks -#ML_HOME=/usr/local/mlworks/bin -#ML_OPTIONS="" +# Moscow ML 2.00 or later (experimental!) +#ML_SYSTEM=mosml +#ML_HOME=$ISABELLE_HOME/../mosml/bin #ML_PLATFORM="" +#ML_OPTIONS="" -# Poly/ML 2.x -#ML_SYSTEM=polyml-2.07 -#ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2 -#ML_OPTIONS="-h 30000" +# MLWorks 2.0 +#ML_SYSTEM=mlworks +#ML_HOME=$ISABELLE_HOME/../mlworks/bin +#ML_OPTIONS="" #ML_PLATFORM="" # Standard ML of New Jersey 0.93