Admin/polyml/settings
changeset 67017 ce6454669360
parent 66899 8176914dae84
child 67099 3345d53e7c58
     1.1 --- a/Admin/polyml/settings	Mon Nov 06 17:21:32 2017 +0100
     1.2 +++ b/Admin/polyml/settings	Tue Nov 07 10:22:10 2017 +0100
     1.3 @@ -49,19 +49,19 @@
     1.4        case "$ML_PLATFORM" in
     1.5          x86_64-windows)
     1.6            POLYML_EXE="$ML_HOME/poly.exe"
     1.7 -          ML_OPTIONS="-H 1000 --codepage utf8"
     1.8 +          ML_OPTIONS="--minheap 2000 --codepage utf8"
     1.9            ;;
    1.10          x86-windows)
    1.11            POLYML_EXE="$ML_HOME/poly.exe"
    1.12 -          ML_OPTIONS="-H 500 --codepage utf8"
    1.13 +          ML_OPTIONS="--minheap 1000 --codepage utf8"
    1.14            ;;
    1.15          x86_64-*)
    1.16            POLYML_EXE="$ML_HOME/poly"
    1.17 -          ML_OPTIONS="-H 1000"
    1.18 +          ML_OPTIONS="--minheap 2000"
    1.19            ;;
    1.20          *)
    1.21            POLYML_EXE="$ML_HOME/poly"
    1.22 -          ML_OPTIONS="-H 500"
    1.23 +          ML_OPTIONS="--minheap 1000"
    1.24            ;;
    1.25        esac
    1.26