equal
deleted
inserted
replaced
12 |
12 |
13 # Note that ML_HOME specifies the location of the actual compiler |
13 # Note that ML_HOME specifies the location of the actual compiler |
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 and 4.0 or later |
17 # Poly/ML 3.x, 4.0, 4.1, and 4.1.1 |
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.1 on x86-linux ... |
19 #maybe a shrink-wrapped polyml-4.1.1 on x86-linux ... |
20 ML_SYSTEM=polyml-4.1.1 |
20 ML_SYSTEM=polyml-4.1.1 |
21 ML_PLATFORM=x86-linux |
21 ML_PLATFORM=x86-linux |
22 ML_HOME=/usr/bin |
22 ML_HOME=/usr/bin |
118 |
118 |
119 # Site settings check -- just to make it a little bit harder to copy this file! |
119 # Site settings check -- just to make it a little bit harder to copy this file! |
120 [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ |
120 [ -n "$ISABELLE_SITE_SETTINGS_PRESENT" ] && \ |
121 { echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; } |
121 { echo >&2 "### Isabelle site settings already present! Maybe copied etc/settings in full?"; } |
122 |
122 |
123 # Users may want to change this. |
123 # Users may want to override this. |
124 ISABELLE_LOGIC=HOL |
124 ISABELLE_LOGIC=HOL |
125 |
125 |
126 |
126 |
127 ## Docs |
127 ## Docs |
128 |
128 |