etc/settings
changeset 9252 83060e826e02
parent 9236 899b83e8d2e1
child 9569 68400ff46b09
equal deleted inserted replaced
9251:bd57acd44fc1 9252:83060e826e02
    25 #ML_SYSTEM=smlnj-110
    25 #ML_SYSTEM=smlnj-110
    26 #ML_HOME=$ISABELLE_HOME/../smlnj/bin
    26 #ML_HOME=$ISABELLE_HOME/../smlnj/bin
    27 #ML_OPTIONS="@SMLdebug=/dev/null"
    27 #ML_OPTIONS="@SMLdebug=/dev/null"
    28 #ML_PLATFORM=$(eval $($ML_HOME/.arch-n-opsys 2>/dev/null); echo $HEAP_SUFFIX)
    28 #ML_PLATFORM=$(eval $($ML_HOME/.arch-n-opsys 2>/dev/null); echo $HEAP_SUFFIX)
    29 
    29 
    30 # MLWorks 2.0 or later
    30 # Moscow ML 2.00 or later (experimental!)
       
    31 #ML_SYSTEM=mosml
       
    32 #ML_HOME=$ISABELLE_HOME/../mosml/bin
       
    33 #ML_PLATFORM=""
       
    34 #ML_OPTIONS=""
       
    35 
       
    36 # MLWorks 2.0
    31 #ML_SYSTEM=mlworks
    37 #ML_SYSTEM=mlworks
    32 #ML_HOME=/usr/local/mlworks/bin
    38 #ML_HOME=$ISABELLE_HOME/../mlworks/bin
    33 #ML_OPTIONS=""
    39 #ML_OPTIONS=""
    34 #ML_PLATFORM=""
       
    35 
       
    36 # Poly/ML 2.x
       
    37 #ML_SYSTEM=polyml-2.07
       
    38 #ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2
       
    39 #ML_OPTIONS="-h 30000"
       
    40 #ML_PLATFORM=""
    40 #ML_PLATFORM=""
    41 
    41 
    42 # Standard ML of New Jersey 0.93
    42 # Standard ML of New Jersey 0.93
    43 #ML_SYSTEM=smlnj-0.93
    43 #ML_SYSTEM=smlnj-0.93
    44 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src
    44 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src