| author | wenzelm |
| Sun, 19 Jan 2020 14:50:03 +0100 | |
| changeset 71397 | 028edb1e5b99 |
| parent 71396 | c1c61d0d8e7c |
| child 72131 | 284d6c06cbfb |
| permissions | -rw-r--r-- |
| 49000 | 1 |
# -*- shell-script -*- :mode=shellscript: |
2 |
||
| 53686 | 3 |
POLYML_HOME="$COMPONENT" |
4 |
||
| 69704 | 5 |
ML_PLATFORM="${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_PLATFORM64}}"
|
| 49000 | 6 |
|
|
61158
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
wenzelm
parents:
61136
diff
changeset
|
7 |
if grep "ML_system_64.*=.*true" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null |
|
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
wenzelm
parents:
61136
diff
changeset
|
8 |
then |
| 69704 | 9 |
ML_OPTIONS="--minheap 1000" |
|
61158
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
wenzelm
parents:
61136
diff
changeset
|
10 |
else |
| 69704 | 11 |
ML_PLATFORM="${ML_PLATFORM/x86_64/x86_64_32}"
|
12 |
ML_OPTIONS="--minheap 500" |
|
|
61158
ea6a4c8bc722
convenient change of ML system architecture via system option ML_preference_64, which is grepped off-line from stored preferences during bootstrap;
wenzelm
parents:
61136
diff
changeset
|
13 |
fi |
| 49000 | 14 |
|
| 70988 | 15 |
ML_SYSTEM=polyml-5.8.1 |
| 69704 | 16 |
ML_HOME="$POLYML_HOME/$ML_PLATFORM" |
17 |
ML_SOURCES="$POLYML_HOME/src" |
|
|
71396
c1c61d0d8e7c
clarified build_polyml_component: include IDE entry point for ML compiler;
wenzelm
parents:
70988
diff
changeset
|
18 |
|
| 71397 | 19 |
ISABELLE_DOCS_EXAMPLES="$ISABELLE_DOCS_EXAMPLES:\$ML_SOURCES/ROOT.ML" |