src/Tools/jEdit/src/jEdit.props
changeset 56892 1c7552b05466
parent 56879 ee2b61f37ad9
child 56907 0f3c375fd27c
equal deleted inserted replaced
56891:48899c43b07d 56892:1c7552b05466
   241 prev-bracket.shortcut2=C+e C+8
   241 prev-bracket.shortcut2=C+e C+8
   242 print.font=IsabelleText
   242 print.font=IsabelleText
   243 recent-buffer.shortcut2=C+CIRCUMFLEX
   243 recent-buffer.shortcut2=C+CIRCUMFLEX
   244 restore.remote=false
   244 restore.remote=false
   245 restore=false
   245 restore=false
       
   246 search.subdirs.toggle=true
   246 select-block.shortcut2=C+8
   247 select-block.shortcut2=C+8
   247 sidekick-tree.dock-position=right
   248 sidekick-tree.dock-position=right
   248 sidekick.auto-complete-popup-get-focus=true
   249 sidekick.auto-complete-popup-get-focus=true
   249 sidekick.buffer-save-parse=true
   250 sidekick.buffer-save-parse=true
   250 sidekick.complete-delay=0
   251 sidekick.complete-delay=0