changeset 28659 | b4fd14ae8b8a |
parent 28658 | a03ae929d9c0 |
child 28914 | f993cbffc42a |
1.1 --- a/etc/settings Tue Oct 21 22:21:28 2008 +0200 1.2 +++ b/etc/settings Tue Oct 21 23:54:42 2008 +0200 1.3 @@ -237,7 +237,8 @@ 1.4 "/opt/jedit" \ 1.5 "") 1.6 1.7 -JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx512m" 1.8 +JEDIT_JAVA_OPTIONS="" 1.9 +#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx512m" 1.10 JEDIT_OPTIONS="-reuseview -noserver -nobackground" 1.11 1.12