# HG changeset patch
# User wenzelm
# Date 1609935388 -3600
# Node ID b34d24153a4784d3fbf5c5fee6596c99dff36e9e
# Parent  66d775f7a6e8ad656c01aa5729e4ef4460eed6ac
sort lines;

diff -r 66d775f7a6e8 -r b34d24153a47 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