etc/settings
changeset 5659 e2a2be6089b4
parent 5387 8f1157817bb6
child 5708 fb09ab6a447f
equal deleted inserted replaced
5658:082debccf486 5659:e2a2be6089b4
    35 # Standard ML of New Jersey 110 or later
    35 # Standard ML of New Jersey 110 or later
    36 #ML_SYSTEM=smlnj-110
    36 #ML_SYSTEM=smlnj-110
    37 #ML_HOME=/usr/local/smlnj-110/bin
    37 #ML_HOME=/usr/local/smlnj-110/bin
    38 #ML_OPTIONS="@SMLdebug=/dev/null"
    38 #ML_OPTIONS="@SMLdebug=/dev/null"
    39 
    39 
    40 # MLWorks 1.0r2 or later -- still EXPERIMENTAL!!
    40 # MLWorks 1.0r2 or later (2.0 recommended)
    41 #ML_SYSTEM=mlworks
    41 #ML_SYSTEM=mlworks
    42 #ML_HOME=/usr/local/mlworks/bin
    42 #ML_HOME=/usr/local/mlworks/bin
    43 #ML_OPTIONS=""
    43 #ML_OPTIONS=""
    44 
    44 
    45 
    45