# HG changeset patch
# User wenzelm
# Date 1518892638 -3600
# Node ID 27f3dceb5a70486c65bb21d08150eb75e6334782
# Parent  85582dded91293901e7249a5e61b9a9df95fd185
avoid conflict with Isabelle/jEdit completion of '>', e.g. "-->", "==>";

diff -r 85582dded912 -r 27f3dceb5a70 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Sat Feb 17 18:42:26 2018 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Sat Feb 17 19:37:18 2018 +0100
@@ -311,3 +311,4 @@
 view.thickCaret=true
 view.title=Isabelle/jEdit -\u0020
 view.width=1072
+xml-insert-closing-tag.shortcut=