changeset 28658 | a03ae929d9c0 |
parent 28657 | 16bbb7fabe0e |
child 28659 | b4fd14ae8b8a |
--- a/etc/settings Tue Oct 21 21:59:22 2008 +0200 +++ b/etc/settings Tue Oct 21 22:21:28 2008 +0200 @@ -238,7 +238,7 @@ "") JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx512m" -JEDIT_OPTIONS="-reuseview -noserver -nobackground '-settings=$ISABELLE_HOME_USER/jedit'" +JEDIT_OPTIONS="-reuseview -noserver -nobackground" ###