changeset 45057 | 86c9b73158a8 |
parent 45024 | 77c3e74bd954 |
child 45636 | 202071bb7f86 |
--- a/src/Tools/jEdit/etc/settings Fri Sep 23 14:12:09 2011 +0200 +++ b/src/Tools/jEdit/etc/settings Fri Sep 23 14:13:15 2011 +0200 @@ -10,7 +10,7 @@ JEDIT_STYLE_SHEETS="$ISABELLE_HOME/etc/isabelle.css:$JEDIT_HOME/etc/isabelle-jedit.css:$ISABELLE_HOME_USER/etc/isabelle.css:$ISABELLE_HOME_USER/etc/isabelle-jedit.css" -ISABELLE_JEDIT_OPTIONS="-m no_brackets -m no_type_brackets" +ISABELLE_JEDIT_OPTIONS="" ISABELLE_TOOLS="$ISABELLE_TOOLS:$JEDIT_HOME/lib/Tools"