added mlworks;
authorwenzelm
Wed, 17 Dec 1997 17:59:18 +0100
changeset 4432a8f5293f7cbc
parent 4431 22f31e6e5aad
child 4433 960868c0cbdd
added mlworks;
etc/settings
     1.1 --- a/etc/settings	Wed Dec 17 17:51:39 1997 +0100
     1.2 +++ b/etc/settings	Wed Dec 17 17:59:18 1997 +0100
     1.3 @@ -37,6 +37,11 @@
     1.4  #ML_HOME=/usr/local/smlnj-110/bin
     1.5  #ML_OPTIONS="@SMLdebug=/dev/null"
     1.6  
     1.7 +# MLWorks 1.0r2 or later -- still EXPERIMENTAL!!
     1.8 +#ML_SYSTEM=mlworks
     1.9 +#ML_HOME=/usr/local/mlworks/bin
    1.10 +#ML_OPTIONS=""
    1.11 +
    1.12  
    1.13  ###
    1.14  ### Compilation options