src/Tools/jEdit/src/jEdit.props
changeset 69644 f044766cd94f
parent 69643 83f15deb2d36
child 69651 2dcfead8fa2e
equal deleted inserted replaced
69643:83f15deb2d36 69644:f044766cd94f
   287 systrayicon=false
   287 systrayicon=false
   288 tip.show=false
   288 tip.show=false
   289 toggle-multi-select.shortcut2=C+NUMBER_SIGN
   289 toggle-multi-select.shortcut2=C+NUMBER_SIGN
   290 toggle-rect-select.shortcut2=A+NUMBER_SIGN
   290 toggle-rect-select.shortcut2=A+NUMBER_SIGN
   291 twoStageSave=false
   291 twoStageSave=false
   292 vfs.browser.dock-position=floating
   292 vfs.browser.dock-position=left
   293 vfs.favorite.0.type=1
   293 vfs.favorite.0.type=1
   294 vfs.favorite.0=$ISABELLE_HOME
   294 vfs.favorite.0=$ISABELLE_HOME
   295 vfs.favorite.1.type=1
   295 vfs.favorite.1.type=1
   296 vfs.favorite.1=$ISABELLE_HOME_USER
   296 vfs.favorite.1=$ISABELLE_HOME_USER
   297 vfs.favorite.2.type=1
   297 vfs.favorite.2.type=1