more favorites;
authorwenzelm
Mon, 14 Jan 2019 14:03:02 +0100
changeset 69651 2dcfead8fa2e
parent 69650 c95edf19133b
child 69653 6b8d78186947
more favorites;
src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Mon Jan 14 13:58:12 2019 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Mon Jan 14 14:03:02 2019 +0100
@@ -298,6 +298,8 @@
 vfs.favorite.2=$JEDIT_HOME
 vfs.favorite.3.type=1
 vfs.favorite.3=$JEDIT_SETTINGS
+vfs.favorite.4.type=1
+vfs.favorite.4=isabelle-export:
 view.antiAlias=standard
 view.blockCaret=true
 view.caretBlink=false