# 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