Differences
This shows you the differences between the selected revisions of the page.
| 2022-11-10 | 2023-03-30 (current) | ||
| drop-down (martin) | 5.14 Bug 1613 Configurable keyboard shortcuts for extensions (martin) | ||
| Line 97: | Line 97: | ||
| </code> | </code> | ||
| - | Produce this options dialog: | + | Produce this options dialog (the [[ui_pref_commands#configure|//Keyboard shortcut// option]] is added implicitly): |
| &screenshotpict(extension_options) | &screenshotpict(extension_options) | ||