# HG changeset patch
# User wenzelm
# Date 1353528500 -3600
# Node ID a29be9d067d2d0db40d96137fc90ab458a15ff8f
# Parent  1f645910e177ae04835ba03b17566a3024828122
tuned comment;

diff -r 1f645910e177 -r a29be9d067d2 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Nov 21 20:50:34 2012 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Nov 21 21:08:20 2012 +0100
@@ -1,7 +1,8 @@
 /*  Title:      Tools/jEdit/src/pretty_text_area.scala
     Author:     Makarius
 
-GUI component for pretty-printed with markup, rendered like jEdit text area.
+GUI component for pretty-printed text with markup, rendered like jEdit
+text area.
 */
 
 package isabelle.jedit