| 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