better accessibility of directory content by typing name prefix;
authorwenzelm
Sun, 07 Apr 2019 16:04:08 +0200
changeset 70077 69465c3e3560
parent 70076 3b3089863eda
child 70079 66dad5805079
better accessibility of directory content by typing name prefix;
src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Sun Apr 07 12:44:37 2019 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Sun Apr 07 16:04:08 2019 +0200
@@ -292,6 +292,7 @@
 toggle-rect-select.shortcut2=A+NUMBER_SIGN
 twoStageSave=false
 vfs.browser.dock-position=left
+vfs.browser.sortMixFilesAndDirs=true
 vfs.favorite.0.type=1
 vfs.favorite.0=$ISABELLE_HOME
 vfs.favorite.1.type=1