# HG changeset patch
# User wenzelm
# Date 1547470982 -3600
# Node ID 2dcfead8fa2ed4d03046b18db5c93c7fa956a849
# Parent  c95edf19133b5d3718dd6f619cc7db4b9da2c2fd
more favorites;

diff -r c95edf19133b -r 2dcfead8fa2e 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