changeset 28657 | 16bbb7fabe0e |
parent 28651 | 0e3f899eb6cf |
child 28658 | a03ae929d9c0 |
--- 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'" ###