# HG changeset patch
# User wenzelm
# Date 1493217011 -7200
# Node ID 3e7bf5e34e0b593558becc9a78f7bf4a525f7057
# Parent  f70c617e9c265aa96f6ab8183143a4548135e2d1
more robust (see also 6688b9cd443b);

diff -r f70c617e9c26 -r 3e7bf5e34e0b src/Pure/Admin/build_log.scala
--- 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)