etc/settings
changeset 4406 9bb6502db2ff
parent 4334 e567f3425267
child 4412 5abf247a238d
equal deleted inserted replaced
4405:b893b3ae8ef3 4406:9bb6502db2ff
    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.09.27 or later
    30 # Standard ML of New Jersey 109.27 to 109.33
    31 #ML_SYSTEM=smlnj-1.09
    31 #ML_SYSTEM=smlnj-109
    32 #ML_HOME=/usr/local/sml109.27/bin
    32 #ML_HOME=/usr/proj/smlnj/109.32/bin
       
    33 #ML_OPTIONS="@SMLdebug=/dev/null"
       
    34 
       
    35 # Standard ML of New Jersey 110 or later
       
    36 #ML_SYSTEM=smlnj-110
       
    37 #ML_HOME=/usr/proj/smlnj/110/bin
    33 #ML_OPTIONS="@SMLdebug=/dev/null"
    38 #ML_OPTIONS="@SMLdebug=/dev/null"
    34 
    39 
    35 
    40 
    36 ###
    41 ###
    37 ### Compilation options
    42 ### Compilation options