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 |
--- a/etc/settings Tue Oct 21 21:22:31 2008 +0200 +++ b/etc/settings Tue Oct 21 21:59:22 2008 +0200 @@ -237,8 +237,8 @@ "/opt/jedit" \ "") -JEDIT_JAVA_OPTIONS="-server -Xms128 -Xmx512" -JEDIT_OPTIONS="-reuseview -noserver -nobackground -settings '$ISABELLE_HOME_USER/jedit'" +JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx512m" +JEDIT_OPTIONS="-reuseview -noserver -nobackground '-settings=$ISABELLE_HOME_USER/jedit'" ###