etc/settings
changeset 8345 e708af969264
parent 7873 5d1200c7a671
child 8880 3a5215883047
equal deleted inserted replaced
8344:4417e588d9f7 8345:e708af969264
     9 ###
     9 ###
    10 
    10 
    11 ## Uncomment and adapt one of the sections below.  Note that ML_HOME
    11 ## Uncomment and adapt one of the sections below.  Note that ML_HOME
    12 ## specifies the location of the actual compiler binaries.
    12 ## specifies the location of the actual compiler binaries.
    13 
    13 
       
    14 # Poly/ML 3.x
       
    15 POLYML_HOME=$ISABELLE_HOME/../polyml
       
    16 ML_PLATFORM=$($POLYML_HOME/bin/polyml-platform 2>/dev/null)
       
    17 ML_HOME=$POLYML_HOME/$ML_PLATFORM
       
    18 ML_SYSTEM=polyml-3.x
       
    19 ML_OPTIONS="-h 30000"
       
    20 
    14 # Standard ML of New Jersey 110 or later
    21 # Standard ML of New Jersey 110 or later
    15 ML_SYSTEM=smlnj-110
    22 #ML_SYSTEM=smlnj-110
    16 ML_HOME=$ISABELLE_HOME/../smlnj/bin
    23 #ML_HOME=$ISABELLE_HOME/../smlnj/bin
    17 ML_OPTIONS="@SMLdebug=/dev/null"
    24 #ML_OPTIONS="@SMLdebug=/dev/null"
    18 ML_PLATFORM=$(eval $($ML_HOME/.arch-n-opsys 2>/dev/null); echo $HEAP_SUFFIX)
    25 #ML_PLATFORM=$(eval $($ML_HOME/.arch-n-opsys 2>/dev/null); echo $HEAP_SUFFIX)
    19 
    26 
    20 # MLWorks 2.0 or later
    27 # MLWorks 2.0 or later
    21 #ML_SYSTEM=mlworks
    28 #ML_SYSTEM=mlworks
    22 #ML_HOME=/usr/local/mlworks/bin
    29 #ML_HOME=/usr/local/mlworks/bin
    23 #ML_OPTIONS=""
    30 #ML_OPTIONS=""
    26 # Poly/ML 2.x
    33 # Poly/ML 2.x
    27 #ML_SYSTEM=polyml-2.07
    34 #ML_SYSTEM=polyml-2.07
    28 #ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2
    35 #ML_HOME=/usr/local/ldist/DIR/polyml/polyml/solaris2
    29 #ML_OPTIONS="-h 30000"
    36 #ML_OPTIONS="-h 30000"
    30 #ML_PLATFORM=""
    37 #ML_PLATFORM=""
    31 
       
    32 # Poly/ML 3.1
       
    33 #ML_SYSTEM=polyml-3.1
       
    34 #ML_HOME=/usr/local/ldist/DIR/polyml-3.1/polyml/sunos5.4
       
    35 #ML_OPTIONS="-h 30000"
       
    36 #ML_PLATFORM=""
       
    37 #LM_LICENSE_FILE=$ML_HOME/license.dat
       
    38 
    38 
    39 # Standard ML of New Jersey 0.93
    39 # Standard ML of New Jersey 0.93
    40 #ML_SYSTEM=smlnj-0.93
    40 #ML_SYSTEM=smlnj-0.93
    41 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src
    41 #ML_HOME=/usr/local/ldist/DIR/sml-0.93/src
    42 #ML_OPTIONS=""
    42 #ML_OPTIONS=""