etc/settings
changeset 32392 d8551606fbab
parent 32332 bc5cec7b2be6
child 32426 dd25b3055c4e
     1.1 --- a/etc/settings	Sat Aug 22 22:31:00 2009 +0200
     1.2 +++ b/etc/settings	Sat Aug 22 23:16:11 2009 +0200
     1.3 @@ -207,22 +207,6 @@
     1.4  
     1.5  
     1.6  ###
     1.7 -### jEdit
     1.8 -###
     1.9 -
    1.10 -JEDIT_HOME=$(choosefrom \
    1.11 -  "$ISABELLE_HOME/contrib/jedit" \
    1.12 -  "$ISABELLE_HOME/../jedit" \
    1.13 -  "/usr/local/jedit" \
    1.14 -  "/usr/share/jedit" \
    1.15 -  "/opt/jedit" \
    1.16 -  "")
    1.17 -
    1.18 -JEDIT_JAVA_OPTIONS=""
    1.19 -#JEDIT_JAVA_OPTIONS="-server -Xms128m -Xmx512m"
    1.20 -JEDIT_OPTIONS="-reuseview -noserver -nobackground"
    1.21 -
    1.22 -###
    1.23  ### External reasoning tools
    1.24  ###
    1.25