tuned JVM settings;
authorwenzelm
Tue Dec 08 12:09:17 2009 +0100 (2009-12-08)
changeset 34756c4818d907ca0
parent 34755 bc255171994b
child 34757 adf4e0f27d54
tuned JVM settings;
src/Tools/jEdit/dist-template/etc/settings
     1.1 --- a/src/Tools/jEdit/dist-template/etc/settings	Mon Dec 07 23:01:13 2009 +0100
     1.2 +++ b/src/Tools/jEdit/dist-template/etc/settings	Tue Dec 08 12:09:17 2009 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4  JEDIT_HOME="$COMPONENT"
     1.5  
     1.6 -JEDIT_JAVA_OPTIONS=""
     1.7 -#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx512m"
     1.8 +JEDIT_JAVA_OPTIONS="-Xms128m -Xmx512m"
     1.9 +#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx1024m"
    1.10  JEDIT_OPTIONS="-reuseview -noserver -nobackground"
    1.11  
    1.12 -ISABELLE_TOOLS="$ISABELLE_TOOLS:$COMPONENT/lib/Tools"
    1.13 +ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"