--- 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