etc/settings
changeset 20987 d1674119d0f9
parent 20764 4aa5c89b933e
child 21171 7b4fb2a2c75e
     1.1 --- a/etc/settings	Wed Oct 11 22:55:23 2006 +0200
     1.2 +++ b/etc/settings	Wed Oct 11 22:56:10 2006 +0200
     1.3 @@ -40,7 +40,7 @@
     1.4  #ML_PLATFORM=x86_64-linux
     1.5  #ML_HOME=/usr/local/polyml/x86_64-linux
     1.6  #ML_SYSTEM=polyml-4.9.1
     1.7 -#ML_OPTIONS="-H 160"
     1.8 +#ML_OPTIONS="-H 500"
     1.9  
    1.10  # Standard ML of New Jersey 110 or later
    1.11  #SMLNJ_CYGWIN_RUNTIME=1