clarified default (amending ca9780325a21): it also affects "open-file" dialog, which should be "buffer";
authorwenzelm
Fri Feb 01 15:02:36 2019 +0100 (3 months ago)
changeset 69781a7529ac9c1c5
parent 69780 b9a5805d1d70
child 69782 76f2d492627e
clarified default (amending ca9780325a21): it also affects "open-file" dialog, which should be "buffer";
src/Tools/jEdit/src/jEdit.props
     1.1 --- a/src/Tools/jEdit/src/jEdit.props	Thu Jan 31 22:53:35 2019 +0100
     1.2 +++ b/src/Tools/jEdit/src/jEdit.props	Fri Feb 01 15:02:36 2019 +0100
     1.3 @@ -290,7 +290,6 @@
     1.4  toggle-multi-select.shortcut2=C+NUMBER_SIGN
     1.5  toggle-rect-select.shortcut2=A+NUMBER_SIGN
     1.6  twoStageSave=false
     1.7 -vfs.browser.defaultPath=favorites
     1.8  vfs.browser.dock-position=left
     1.9  vfs.favorite.0.type=1
    1.10  vfs.favorite.0=$ISABELLE_HOME