src/Tools/jEdit/src/jEdit.props
changeset 53933 7924d61b50cf
parent 53883 f1c5f857df3d
child 54306 2828f17fa41a
     1.1 --- a/src/Tools/jEdit/src/jEdit.props	Thu Sep 26 16:42:18 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/jEdit.props	Thu Sep 26 21:39:10 2013 +0200
     1.3 @@ -1,4 +1,5 @@
     1.4  #jEdit properties
     1.5 +action-bar.shortcut=C+ENTER
     1.6  buffer.deepIndent=false
     1.7  buffer.encoding=UTF-8-Isabelle
     1.8  buffer.indentSize=2