equal
deleted
inserted
replaced
1 # -*- shell-script -*- :mode=shellscript: |
1 # -*- shell-script -*- :mode=shellscript: |
2 |
2 |
3 POLYML_HOME="$COMPONENT" |
3 POLYML_HOME="$COMPONENT" |
4 |
4 |
5 ML_PLATFORM="${ISABELLE_APPLE_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_PLATFORM64}}}" |
5 if [ -n "$ISABELLE_APPLE_PLATFORM64" ] |
|
6 then |
|
7 if grep "ML_system_apple.*=.*false" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null |
|
8 then |
|
9 ML_PLATFORM="$ISABELLE_PLATFORM64" |
|
10 else |
|
11 ML_PLATFORM="$ISABELLE_APPLE_PLATFORM64" |
|
12 fi |
|
13 else |
|
14 ML_PLATFORM="${ISABELLE_WINDOWS_PLATFORM64:-$ISABELLE_PLATFORM64}" |
|
15 fi |
6 |
16 |
7 if grep "ML_system_64.*=.*true" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null |
17 if grep "ML_system_64.*=.*true" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null |
8 then |
18 then |
9 ML_OPTIONS="--minheap 1000" |
19 ML_OPTIONS="--minheap 1000" |
10 else |
20 else |