equal
deleted
inserted
replaced
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 |