favorites for jEdit file browser, although an expanded directory path is expected here, not environment variables;
authorwenzelm
Tue, 22 Apr 2014 12:41:34 +0200
changeset 56632 b3a2dedcc9ec
parent 56631 89269bb8e7ca
child 56633 18f50d5f84ef
child 56658 86f9c6912965
favorites for jEdit file browser, although an expanded directory path is expected here, not environment variables;
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