etc/settings
changeset 3349 943d1630f003
parent 3312 6ec687d436aa
child 3362 0b268cff9344
equal deleted inserted replaced
3348:3f9a806f061e 3349:943d1630f003
    30 # Standard ML of New Jersey 1.07
    30 # Standard ML of New Jersey 1.07
    31 #ML_SYSTEM=smlnj-1.07
    31 #ML_SYSTEM=smlnj-1.07
    32 #ML_HOME=/usr/local/sml107/bin
    32 #ML_HOME=/usr/local/sml107/bin
    33 #ML_OPTIONS="@SMLdebug=/dev/null"
    33 #ML_OPTIONS="@SMLdebug=/dev/null"
    34 
    34 
    35 # Standard ML of New Jersey 1.09.27
    35 # Standard ML of New Jersey 1.09.27, or later
    36 #ML_SYSTEM=smlnj-1.09
    36 #ML_SYSTEM=smlnj-1.09
    37 #ML_HOME=/usr/local/sml109.27/bin
    37 #ML_HOME=/usr/local/sml109.27/bin
    38 #ML_OPTIONS="@SMLdebug=/dev/null"
    38 #ML_OPTIONS="@SMLdebug=/dev/null"
    39 
    39 
    40 
    40