clarified view.title;
authorwenzelm
Sat, 30 Nov 2013 17:38:08 +0100
changeset 553036a35bc1ee210
parent 55302 e38592fa2830
child 55304 9e8189a841f7
clarified view.title;
src/Tools/jEdit/src/jEdit.props
     1.1 --- a/src/Tools/jEdit/src/jEdit.props	Sat Nov 30 17:26:00 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/jEdit.props	Sat Nov 30 17:38:08 2013 +0100
     1.3 @@ -264,4 +264,5 @@
     1.4  view.middleMousePaste=true
     1.5  view.showToolbar=false
     1.6  view.thickCaret=true
     1.7 +view.title=Isabelle/jEdit -\u0020
     1.8  view.width=1072