# HG changeset patch
# User wenzelm
# Date 1398163294 -7200
# Node ID b3a2dedcc9ec1434b64e7f40a65d4ffa18bcfe40
# Parent  89269bb8e7ca1cc24892445e5f9717fb2880761e
favorites for jEdit file browser, although an expanded directory path is expected here, not environment variables;

diff -r 89269bb8e7ca -r b3a2dedcc9ec src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Tue Apr 22 12:30:54 2014 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Tue Apr 22 12:41:34 2014 +0200
@@ -258,6 +258,10 @@
 toggle-rect-select.shortcut2=A+NUMBER_SIGN
 twoStageSave=false
 vfs.browser.dock-position=floating
+vfs.favorite.0=$ISABELLE_HOME
+vfs.favorite.0.type=1
+vfs.favorite.1=$ISABELLE_HOME_USER
+vfs.favorite.1.type=1
 view.antiAlias=standard
 view.blockCaret=true
 view.caretBlink=false