src/Tools/jEdit/src/jEdit.props
changeset 68080 17f79ae49401
parent 68067 b91c4acc1aaf
child 69343 395c4fb15ea2
--- a/src/Tools/jEdit/src/jEdit.props	Fri May 04 15:59:21 2018 +0200
+++ b/src/Tools/jEdit/src/jEdit.props	Fri May 04 16:22:09 2018 +0200
@@ -310,6 +310,5 @@
 view.middleMousePaste=true
 view.showToolbar=true
 view.thickCaret=true
-view.title=Isabelle/jEdit -\u0020
 view.width=1072
 xml-insert-closing-tag.shortcut=