etc/settings
changeset 3182 3270d7bca923
parent 3177 3c1448b9b0ee
child 3184 4e0bbfb113d5
equal deleted inserted replaced
3181:3f7f4a7ae1d1 3182:3270d7bca923
    15 #ML_SYSTEM=polyml-2.07
    15 #ML_SYSTEM=polyml-2.07
    16 #ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2
    16 #ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2
    17 #ML_OPTIONS="-h 30000"
    17 #ML_OPTIONS="-h 30000"
    18 
    18 
    19 # Poly/ML 3.1
    19 # Poly/ML 3.1
    20 #ML_SYSTEM=polyml-3.1
    20 ML_SYSTEM=polyml-3.1
    21 #ML_HOME=/usr/local/ldist/DIR/polyml-3.1/polyml/sunos5.4
    21 ML_HOME=/usr/local/ldist/DIR/polyml-3.1/polyml/sunos5.4
    22 #ML_OPTIONS="-h 30000"
    22 ML_OPTIONS="-h 30000"
    23 #LM_LICENSE_FILE=$ML_HOME/license.dat
    23 LM_LICENSE_FILE=$ML_HOME/license.dat
    24 
    24 
    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=""
    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
    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 
    41 ###
    41 ###
    42 ### Compilation options
    42 ### Compilation options
    43 ###
    43 ###