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_WINDOWS_PLATFORM64:-${ISABELLE_PLATFORM64}}" |
5 ML_PLATFORM="${ISABELLE_APPLE_PLATFORM64:-${ISABELLE_WINDOWS_PLATFORM64:-${ISABELLE_PLATFORM64}}}" |
6 |
6 |
7 if grep "ML_system_64.*=.*true" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null |
7 if grep "ML_system_64.*=.*true" "$ISABELLE_HOME_USER/etc/preferences" >/dev/null 2>/dev/null |
8 then |
8 then |
9 ML_OPTIONS="--minheap 1000" |
9 ML_OPTIONS="--minheap 1000" |
10 else |
10 else |