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" \ |