etc/settings
changeset 3596 c44c83006891
parent 3364 8f225296fade
child 3637 02ba2acc69c3
equal deleted inserted replaced
3595:fb25f00d1c70 3596:c44c83006891
    25 # Standard ML of New Jersey 0.93
    25 # Standard ML of New Jersey 0.93
    26 #ML_SYSTEM=smlnj-0.93
    26 #ML_SYSTEM=smlnj-0.93
    27 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src
    27 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src
    28 #ML_OPTIONS=""
    28 #ML_OPTIONS=""
    29 
    29 
    30 # Standard ML of New Jersey 1.07
    30 # Standard ML of New Jersey 1.09.27 or later
    31 #ML_SYSTEM=smlnj-1.07
       
    32 #ML_HOME=/usr/local/sml107/bin
       
    33 #ML_OPTIONS="@SMLdebug=/dev/null"
       
    34 
       
    35 # Standard ML of New Jersey 1.09.27, 1.09.28, or later
       
    36 #ML_SYSTEM=smlnj-1.09
    31 #ML_SYSTEM=smlnj-1.09
    37 #ML_HOME=/usr/local/sml109.27/bin
    32 #ML_HOME=/usr/local/sml109.27/bin
    38 #ML_OPTIONS="@SMLdebug=/dev/null"
    33 #ML_OPTIONS="@SMLdebug=/dev/null"
    39 
    34 
    40 
    35