diff -r 73d53ad05b14 -r 8f5fbe4a80ff src/Tools/jEdit/dist-template/etc/settings
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/dist-template/etc/settings	Sat Aug 22 23:17:09 2009 +0200
@@ -0,0 +1,7 @@
+JEDIT_HOME="$COMPONENT"
+
+JEDIT_JAVA_OPTIONS=""
+#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx512m"
+JEDIT_OPTIONS="-reuseview -noserver -nobackground"
+
+ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"