# HG changeset patch
# User wenzelm
# Date 1583247117 -3600
# Node ID f79d57c27919a6972070e1b7a59bc21f1d6f4f2a
# Parent  948143567b03e84309729be3927c68508a84c4d3
avoid conflict with isabelle.next-error, resulting in odd startup dialog;

diff -r 948143567b03 -r f79d57c27919 src/Tools/jEdit/src/jEdit.props
--- 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