etc/settings
changeset 4413 0d246395e311
parent 4412 5abf247a238d
child 4432 a8f5293f7cbc
equal deleted inserted replaced
4412:5abf247a238d 4413:0d246395e311
    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 
    40 
    41 ###
    41 ###
    42 ### Compilation options
    42 ### Compilation options
    43 ###
    43 ###
    61 
    61 
    62 # Heap file locations. ML system identifier appended automatically!
    62 # Heap file locations. ML system identifier appended automatically!
    63 
    63 
    64 ISABELLE_PATH=$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps
    64 ISABELLE_PATH=$ISABELLE_HOME_USER/heaps:$ISABELLE_HOME/heaps
    65 
    65 
    66 #A hack! Isabelle build tells us to store heaps within the distribution.
    66 #A hack! Isabelle build tells us to store heaps etc. within the
       
    67 #distribution.
    67 if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then
    68 if [ "$THIS_IS_ISABELLE_BUILD" = true ]; then
    68   ISABELLE_OUTPUT=$ISABELLE_HOME/heaps
    69   ISABELLE_OUTPUT=$ISABELLE_HOME/heaps
    69   ISABELLE_BROWSER_INFO=$ISABELLE_HOME/browser_info
    70   ISABELLE_BROWSER_INFO=$ISABELLE_HOME/browser_info
    70 else
    71 else
    71   ISABELLE_OUTPUT=$ISABELLE_HOME_USER/heaps
    72   ISABELLE_OUTPUT=$ISABELLE_HOME_USER/heaps