# HG changeset patch
# User wenzelm
# Date 1224626082 -7200
# Node ID b4fd14ae8b8a0f66e15a5cc60b7929e5bbaa0b42
# Parent  a03ae929d9c071046dd170d5688b0dc1799a0593
less ambitious default for JEDIT_JAVA_OPTIONS;

diff -r a03ae929d9c0 -r b4fd14ae8b8a etc/settings
--- a/etc/settings	Tue Oct 21 22:21:28 2008 +0200
+++ b/etc/settings	Tue Oct 21 23:54:42 2008 +0200
@@ -237,7 +237,8 @@
   "/opt/jedit" \
   "")
 
-JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx512m"
+JEDIT_JAVA_OPTIONS=""
+#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx512m"
 JEDIT_OPTIONS="-reuseview -noserver -nobackground"