etc/settings
changeset 4569 4fd775d5456f
parent 4544 bd3307d3e974
child 4579 4f1e445b20d7
equal deleted inserted replaced
4568:7be03035c553 4569:4fd775d5456f
    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-109
    31 #ML_SYSTEM=smlnj-109
    32 #ML_HOME=/usr/proj/smlnj/109.32/bin
    32 #ML_HOME=/usr/proj/smlnj/109.32/bin
    33 #ML_OPTIONS="@SMLdebug=/dev/null"
    33 #ML_OPTIONS="@SMLdebug=/dev/null"
    34 
    34 
    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 -- still EXPERIMENTAL!!
    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=""