src/Tools/jEdit/src/jEdit.props
changeset 63726 dd327befd2ef
parent 63455 019856db2bb6
child 63737 fb0ae6b60491
equal deleted inserted replaced
63725:4c00ba1ad11a 63726:dd327befd2ef
   253 plugin-blacklist.MacOSX.jar=true
   253 plugin-blacklist.MacOSX.jar=true
   254 plugin.MacOSXPlugin.altDispatcher=false
   254 plugin.MacOSXPlugin.altDispatcher=false
   255 plugin.MacOSXPlugin.disableOption=true
   255 plugin.MacOSXPlugin.disableOption=true
   256 prev-bracket.shortcut2=C+e C+8
   256 prev-bracket.shortcut2=C+e C+8
   257 print.font=IsabelleText
   257 print.font=IsabelleText
       
   258 print.glyphVector=true
   258 recent-buffer.shortcut2=C+CIRCUMFLEX
   259 recent-buffer.shortcut2=C+CIRCUMFLEX
   259 restore.remote=false
   260 restore.remote=false
   260 restore=false
   261 restore=false
   261 search.subdirs.toggle=true
   262 search.subdirs.toggle=true
   262 select-block.shortcut2=C+8
   263 select-block.shortcut2=C+8