author | wenzelm |
Wed, 06 Jan 2021 13:16:28 +0100 | |
changeset 73080 | b34d24153a47 |
parent 73079 | 66d775f7a6e8 |
child 73081 | 120ffea2c244 |
--- a/src/Tools/jEdit/src/jEdit.props Wed Jan 06 13:00:31 2021 +0100 +++ b/src/Tools/jEdit/src/jEdit.props Wed Jan 06 13:16:28 2021 +0100 @@ -276,8 +276,8 @@ metal.secondary.font=Isabelle DejaVu Sans metal.secondary.fontsize=12 navigator.showOnToolbar=true +new-file-in-mode.shortcut= next-bracket.shortcut2=C+e C+9 -new-file-in-mode.shortcut= options.shortcuts.deletekeymap.label=Delete options.shortcuts.duplicatekeymap.dialog.title=Keymap name options.shortcuts.duplicatekeymap.label=Duplicate