author | wenzelm |
Mon, 16 Dec 1996 10:28:50 +0100 | |
changeset 2410 | a0727e4d9453 |
parent 2409 | f4505fe0bd22 |
child 2411 | 256dbda3df4f |
etc/settings | file | annotate | diff | comparison | revisions |
--- a/etc/settings Mon Dec 16 10:05:16 1996 +0100 +++ b/etc/settings Mon Dec 16 10:28:50 1996 +0100 @@ -45,7 +45,7 @@ ## ML compilers and options -#ML_SYSTEM=polyml-2.07 +#ML_SYSTEM=polyml-2.x #ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2 #ML_OPTIONS="-h 30000" @@ -55,6 +55,8 @@ LM_LICENSE_FILE=$ML_HOME/license.dat #ML_SYSTEM=smlnj-0.93 +#ML_HOME=/usr/local/ldist/DIR/sml-0.93/src +#ML_OPTIONS="" #ML_SYSTEM=smlnj-1.07 #ML_HOME=/usr/local/sml107