author | wenzelm |
Tue, 03 Mar 2020 15:51:57 +0100 | |
changeset 71511 | f79d57c27919 |
parent 71510 | 948143567b03 |
child 71512 | fe93a863d946 |
child 71513 | a403942212f2 |
--- a/src/Tools/jEdit/src/jEdit.props Tue Mar 03 15:51:02 2020 +0100 +++ b/src/Tools/jEdit/src/jEdit.props Tue Mar 03 15:51:57 2020 +0100 @@ -271,6 +271,7 @@ metal.secondary.font=Isabelle DejaVu Sans navigator.showOnToolbar=true 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