# HG changeset patch
# User wenzelm
# Date 1289943645 -3600
# Node ID 2315c3daee74e9ac41ae27f41fe8ac03776db741
# Parent  fbac01813bff852bb514686fa19e348bec977bd3
avoid spam;

diff -r fbac01813bff -r 2315c3daee74 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Nov 16 22:13:54 2010 +0100
+++ b/src/Pure/PIDE/command.scala	Tue Nov 16 22:40:45 2010 +0100
@@ -54,7 +54,9 @@
                 val props = Position.purge(atts)
                 val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
                 state.add_markup(info)
-              case _ => System.err.println("Ignored report message: " + msg); state
+              case _ =>
+                // FIXME System.err.println("Ignored report message: " + msg)
+                state
             })
         case XML.Elem(Markup(name, atts), body) =>
           atts match {