# HG changeset patch # User wenzelm # Date 850728530 -3600 # Node ID a0727e4d94534f6ae5d6722b16c5698b769c546c # Parent f4505fe0bd22606c6a4ec36593b929ac8e401236 added smlnj-0.93; diff -r f4505fe0bd22 -r a0727e4d9453 etc/settings --- 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