src/Pure/System/session.scala
changeset 50255 d0ec1f0d1d7d
parent 50201 c26369c9eda6
child 50344 608265769ce0
--- a/src/Pure/System/session.scala	Wed Nov 28 16:09:05 2012 +0100
+++ b/src/Pure/System/session.scala	Wed Nov 28 17:18:53 2012 +0100
@@ -358,6 +358,9 @@
             case None =>
           }
 
+        case Markup.ML_Statistics(stats) if output.is_protocol =>
+          java.lang.System.err.println(stats.toString)  // FIXME
+
         case _ if output.is_init =>
             phase = Session.Ready