# HG changeset patch # User wenzelm # Date 909256881 -7200 # Node ID 6af1272cbd53460b1e6612959bc0d24274575b9d # Parent b4993fc1de5885ccc81b89a12aaa2ebdb0705204 ML_SYSTEM factory default; diff -r b4993fc1de58 -r 6af1272cbd53 etc/settings --- a/etc/settings Sat Oct 24 20:28:03 1998 +0200 +++ b/etc/settings Sat Oct 24 21:21:21 1998 +0200 @@ -12,9 +12,9 @@ ## specifies the location of the actual compiler binaries. # Standard ML of New Jersey 110 or later -#ML_SYSTEM=smlnj-110 -#ML_HOME=/usr/local/smlnj-110/bin -#ML_OPTIONS="@SMLdebug=/dev/null" +ML_SYSTEM=smlnj-110 +ML_HOME=/usr/local/smlnj-110/bin +ML_OPTIONS="@SMLdebug=/dev/null" # MLWorks 2.0 or later #ML_SYSTEM=mlworks @@ -27,10 +27,10 @@ #ML_OPTIONS="-h 30000" # Poly/ML 3.1 -ML_SYSTEM=polyml-3.1 -ML_HOME=/usr/local/ldist/DIR/polyml-3.1/polyml/sunos5.4 -ML_OPTIONS="-h 30000" -LM_LICENSE_FILE=$ML_HOME/license.dat +#ML_SYSTEM=polyml-3.1 +#ML_HOME=/usr/local/ldist/DIR/polyml-3.1/polyml/sunos5.4 +#ML_OPTIONS="-h 30000" +#LM_LICENSE_FILE=$ML_HOME/license.dat # Standard ML of New Jersey 0.93 #ML_SYSTEM=smlnj-0.93