avoid spam;
authorwenzelm
Tue, 16 Nov 2010 22:40:45 +0100
changeset 40572 2315c3daee74
parent 40571 fbac01813bff
child 40573 113ccf02d323
avoid spam;
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 {