etc/settings
changeset 14447 5b61dc4eab24
parent 14344 0f0a2148a099
child 14451 2253d273d944
equal deleted inserted replaced
14446:0bc2519e9990 14447:5b61dc4eab24
    14 # binaries.  Do not invent new ML system names unless you know what
    14 # binaries.  Do not invent new ML system names unless you know what
    15 # you are doing.  Only one of the sections below should be activated.
    15 # you are doing.  Only one of the sections below should be activated.
    16 
    16 
    17 # Poly/ML 3.x, 4.0, 4.1, 4.1.1, 4.1.2
    17 # Poly/ML 3.x, 4.0, 4.1, 4.1.1, 4.1.2
    18 if [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
    18 if [ -e /usr/bin/poly -a -e /usr/lib/poly ]; then
    19   #maybe a shrink-wrapped polyml-4.1.2 on x86-linux ...
    19   #maybe a shrink-wrapped polyml on x86-linux ...
    20   ML_SYSTEM=polyml-4.1.2
    20 
       
    21   # include version number, needed for choosing right options
       
    22   ML_SYSTEM=polyml-4.1.3    
       
    23   # processor/OS type
    21   ML_PLATFORM=x86-linux
    24   ML_PLATFORM=x86-linux
       
    25   # where to find binaries
    22   ML_HOME=/usr/bin
    26   ML_HOME=/usr/bin
       
    27   # where to find the standard database
    23   ML_DBASE=/usr/lib/poly/ML_dbase
    28   ML_DBASE=/usr/lib/poly/ML_dbase
       
    29   # options to pass to poly
    24   ML_OPTIONS="-h 15000"
    30   ML_OPTIONS="-h 15000"
    25 else
    31 else
    26   #... or rather a self-contained multi-platform installation
    32   #... or rather a self-contained multi-platform installation
    27   POLYML_HOME=$(choosefrom \
    33   POLYML_HOME=$(choosefrom \
    28     "$ISABELLE_HOME/contrib/polyml" \
    34     "$ISABELLE_HOME/contrib/polyml" \