# HG changeset patch
# User wenzelm
# Date 1385829488 -3600
# Node ID 6a35bc1ee21044552a3c85688763cecfa4110059
# Parent  e38592fa283098542c951415c1b9dbfd56e39332
clarified view.title;

diff -r e38592fa2830 -r 6a35bc1ee210 src/Tools/jEdit/src/jEdit.props
--- a/src/Tools/jEdit/src/jEdit.props	Sat Nov 30 17:26:00 2013 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Sat Nov 30 17:38:08 2013 +0100
@@ -264,4 +264,5 @@
 view.middleMousePaste=true
 view.showToolbar=false
 view.thickCaret=true
+view.title=Isabelle/jEdit -\u0020
 view.width=1072