author | wenzelm |
Tue, 21 Oct 2008 21:59:22 +0200 | |
changeset 28657 | 16bbb7fabe0e |
parent 28656 | e92c79b3b154 |
child 28658 | a03ae929d9c0 |
etc/settings | file | annotate | diff | comparison | revisions |
1.1 --- a/etc/settings Tue Oct 21 21:22:31 2008 +0200 1.2 +++ b/etc/settings Tue Oct 21 21:59:22 2008 +0200 1.3 @@ -237,8 +237,8 @@ 1.4 "/opt/jedit" \ 1.5 "") 1.6 1.7 -JEDIT_JAVA_OPTIONS="-server -Xms128 -Xmx512" 1.8 -JEDIT_OPTIONS="-reuseview -noserver -nobackground -settings '$ISABELLE_HOME_USER/jedit'" 1.9 +JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx512m" 1.10 +JEDIT_OPTIONS="-reuseview -noserver -nobackground '-settings=$ISABELLE_HOME_USER/jedit'" 1.11 1.12 1.13 ###