src/Tools/jEdit/src/jEdit.props
changeset 67647 27f3dceb5a70
parent 67132 336831647779
child 68068 b91c4acc1aaf
     1.1 --- a/src/Tools/jEdit/src/jEdit.props	Sat Feb 17 18:42:26 2018 +0100
     1.2 +++ b/src/Tools/jEdit/src/jEdit.props	Sat Feb 17 19:37:18 2018 +0100
     1.3 @@ -311,3 +311,4 @@
     1.4  view.thickCaret=true
     1.5  view.title=Isabelle/jEdit -\u0020
     1.6  view.width=1072
     1.7 +xml-insert-closing-tag.shortcut=