sort lines;
authorwenzelm
Wed, 06 Jan 2021 13:16:28 +0100
changeset 73080 b34d24153a47
parent 73079 66d775f7a6e8
child 73081 120ffea2c244
sort lines;
src/Tools/jEdit/src/jEdit.props
--- 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