--- a/src/Tools/jEdit/src/jEdit.props Thu Sep 26 16:42:18 2013 +0200
+++ b/src/Tools/jEdit/src/jEdit.props Thu Sep 26 21:39:10 2013 +0200
@@ -1,4 +1,5 @@
#jEdit properties
+action-bar.shortcut=C+ENTER
buffer.deepIndent=false
buffer.encoding=UTF-8-Isabelle
buffer.indentSize=2