1.1 --- a/etc/settings Wed May 14 15:28:37 1997 +0200
1.2 +++ b/etc/settings Wed May 14 17:41:15 1997 +0200
1.3 @@ -17,10 +17,10 @@
1.4 #ML_OPTIONS="-h 30000"
1.5
1.6 # Poly/ML 3.1
1.7 -#ML_SYSTEM=polyml-3.1
1.8 -#ML_HOME=/usr/local/ldist/DIR/polyml-3.1/polyml/sunos5.4
1.9 -#ML_OPTIONS="-h 30000"
1.10 -#LM_LICENSE_FILE=$ML_HOME/license.dat
1.11 +ML_SYSTEM=polyml-3.1
1.12 +ML_HOME=/usr/local/ldist/DIR/polyml-3.1/polyml/sunos5.4
1.13 +ML_OPTIONS="-h 30000"
1.14 +LM_LICENSE_FILE=$ML_HOME/license.dat
1.15
1.16 # Standard ML of New Jersey 0.93
1.17 #ML_SYSTEM=smlnj-0.93
1.18 @@ -33,9 +33,9 @@
1.19 #ML_OPTIONS="@SMLdebug=/dev/null"
1.20
1.21 # Standard ML of New Jersey 1.09.27
1.22 -ML_SYSTEM=smlnj-1.09
1.23 -ML_HOME=/usr/local/sml109.27/bin
1.24 -ML_OPTIONS="@SMLdebug=/dev/null"
1.25 +#ML_SYSTEM=smlnj-1.09
1.26 +#ML_HOME=/usr/local/sml109.27/bin
1.27 +#ML_OPTIONS="@SMLdebug=/dev/null"
1.28
1.29
1.30 ###