--- a/src/Pure/Admin/build_log.scala Wed Apr 26 16:13:05 2017 +0200
+++ b/src/Pure/Admin/build_log.scala Wed Apr 26 16:30:11 2017 +0200
@@ -505,7 +505,7 @@
case Heap(name, Value.Long(size)) =>
heap_sizes += (name -> size)
- case _ if line.startsWith(ML_STATISTICS_MARKER) =>
+ case _ if line.startsWith(ML_STATISTICS_MARKER) && YXML.detect(line) =>
val (name, props) =
Library.try_unprefix(ML_STATISTICS_MARKER, line).map(log_file.parse_props(_)) match {
case Some((SESSION_NAME, session_name) :: props) => (session_name, props)