# HG changeset patch
# User wenzelm
# Date 1392745411 -3600
# Node ID d77090e07000fb96de0d7c1f8838a0647e1025ca
# Parent  99409ccbe04ab10143e2e95e4809a930c86cfb3b
tuned whitespace;

diff -r 99409ccbe04a -r d77090e07000 src/Pure/PIDE/yxml.scala
--- a/src/Pure/PIDE/yxml.scala	Tue Feb 18 18:29:02 2014 +0100
+++ b/src/Pure/PIDE/yxml.scala	Tue Feb 18 18:43:31 2014 +0100
@@ -33,7 +33,7 @@
     def tree(t: XML.Tree): Unit =
       t match {
         case XML.Elem(Markup(name, atts), ts) =>
-          s += X; s += Y; s++= name; atts.foreach(attrib); s += X
+          s += X; s += Y; s ++= name; atts.foreach(attrib); s += X
           ts.foreach(tree)
           s += X; s += Y; s += X
         case XML.Text(text) => s ++= text