# HG changeset patch
# User wenzelm
# Date 1493715904 -7200
# Node ID 45632d594bdb912e02ee62250a58025b3ef6f396
# Parent  aaba2e0c247c2226b8a9759c9a21a34c8358d82a
more general pattern;

diff -r aaba2e0c247c -r 45632d594bdb src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue May 02 10:47:39 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Tue May 02 11:05:04 2017 +0200
@@ -533,7 +533,7 @@
     val Session_Finished2 =
       new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
     val Session_Timing =
-      new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
+      new Regex("""^Timing (\S+) \((\d+) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
     val Session_Started = new Regex("""^(?:Running|Building) (\S+) \.\.\.$""")
     val Session_Failed = new Regex("""^(\S+) FAILED""")
     val Session_Cancelled = new Regex("""^(\S+) CANCELLED""")