# HG changeset patch
# User wenzelm
# Date 1446219097 -3600
# Node ID c0429568593679906b7582224888e165c56a3dc0
# Parent  f2e51e704a962fbdb3f62b28a11c73eabc62d97f
obsolete (see 9c6346319eee, 7924d61b50cf);

diff -r f2e51e704a96 -r c04295685936 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Thu Oct 29 15:40:52 2015 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Fri Oct 30 16:31:37 2015 +0100
@@ -1,5 +1,4 @@
 #jEdit properties
-action-bar.shortcut=C+ENTER
 buffer.deepIndent=false
 buffer.encoding=UTF-8-Isabelle
 buffer.indentSize=2