etc/settings
changeset 6413 b2f2770ef8d9
parent 5964 a825c5929f4f
child 6462 d5cc7c304db0
equal deleted inserted replaced
6412:9309bc455432 6413:b2f2770ef8d9
    13 
    13 
    14 # Standard ML of New Jersey 110 or later
    14 # Standard ML of New Jersey 110 or later
    15 #ML_SYSTEM=smlnj-110
    15 #ML_SYSTEM=smlnj-110
    16 #ML_HOME=/usr/local/smlnj-110/bin
    16 #ML_HOME=/usr/local/smlnj-110/bin
    17 #ML_OPTIONS="@SMLdebug=/dev/null"
    17 #ML_OPTIONS="@SMLdebug=/dev/null"
       
    18 #ML_PLATFORM=$(eval $($ML_HOME/.arch-n-opsys); echo $HEAP_SUFFIX)
    18 
    19 
    19 # MLWorks 2.0 or later
    20 # MLWorks 2.0 or later
    20 #ML_SYSTEM=mlworks
    21 #ML_SYSTEM=mlworks
    21 #ML_HOME=/usr/local/mlworks/bin
    22 #ML_HOME=/usr/local/mlworks/bin
    22 #ML_OPTIONS=""
    23 #ML_OPTIONS=""
       
    24 #ML_PLATFORM=""
    23 
    25 
    24 # Poly/ML 2.x
    26 # Poly/ML 2.x
    25 #ML_SYSTEM=polyml-2.07
    27 #ML_SYSTEM=polyml-2.07
    26 #ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2
    28 #ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2
    27 #ML_OPTIONS="-h 30000"
    29 #ML_OPTIONS="-h 30000"
       
    30 #ML_PLATFORM=""
    28 
    31 
    29 # Poly/ML 3.1
    32 # Poly/ML 3.1
    30 ML_SYSTEM=polyml-3.1
    33 ML_SYSTEM=polyml-3.1
    31 ML_HOME=/usr/local/ldist/DIR/polyml-3.1/polyml/sunos5.4
    34 ML_HOME=/usr/local/ldist/DIR/polyml-3.1/polyml/sunos5.4
    32 ML_OPTIONS="-h 30000"
    35 ML_OPTIONS="-h 30000"
       
    36 ML_PLATFORM=""
    33 LM_LICENSE_FILE=$ML_HOME/license.dat
    37 LM_LICENSE_FILE=$ML_HOME/license.dat
    34 
    38 
    35 # Standard ML of New Jersey 0.93
    39 # Standard ML of New Jersey 0.93
    36 #ML_SYSTEM=smlnj-0.93
    40 #ML_SYSTEM=smlnj-0.93
    37 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src
    41 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src
    38 #ML_OPTIONS=""
    42 #ML_OPTIONS=""
       
    43 #ML_PLATFORM=""
    39 
    44 
    40 
    45 
    41 ###
    46 ###
    42 ### Compilation options
    47 ### Compilation options
    43 ###
    48 ###