etc/settings
changeset 32392 d8551606fbab
parent 32332 bc5cec7b2be6
child 32426 dd25b3055c4e
--- a/etc/settings	Sat Aug 22 22:31:00 2009 +0200
+++ b/etc/settings	Sat Aug 22 23:16:11 2009 +0200
@@ -207,22 +207,6 @@
 
 
 ###
-### jEdit
-###
-
-JEDIT_HOME=$(choosefrom \
-  "$ISABELLE_HOME/contrib/jedit" \
-  "$ISABELLE_HOME/../jedit" \
-  "/usr/local/jedit" \
-  "/usr/share/jedit" \
-  "/opt/jedit" \
-  "")
-
-JEDIT_JAVA_OPTIONS=""
-#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx512m"
-JEDIT_OPTIONS="-reuseview -noserver -nobackground"
-
-###
 ### External reasoning tools
 ###