# HG changeset patch
# User wenzelm
# Date 1471207703 -7200
# Node ID fed1d4dab990ee9d6671137141d9fc122cfc9d06
# Parent  3744d2cf4d2f31c1c6cbcf0f97f996a1ac3591ac
cpu time is optional (see Timing.message_resources);

diff -r 3744d2cf4d2f -r fed1d4dab990 src/Pure/Tools/build_stats.scala
--- a/src/Pure/Tools/build_stats.scala	Sun Aug 14 22:35:38 2016 +0200
+++ b/src/Pure/Tools/build_stats.scala	Sun Aug 14 22:48:23 2016 +0200
@@ -15,8 +15,10 @@
 {
   /* parse build output */
 
-  private val Session_Finished =
+  private val Session_Finished1 =
     new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time, (\d+):(\d+):(\d+) cpu time.*$""")
+  private val Session_Finished2 =
+    new Regex("""^Finished (\S+) \((\d+):(\d+):(\d+) elapsed time.*$""")
   private val Session_Timing =
     new Regex("""^Timing (\S+) \((\d) threads, (\d+\.\d+)s elapsed time, (\d+\.\d+)s cpu time, (\d+\.\d+)s GC time.*$""")
 
@@ -45,12 +47,16 @@
 
     for (line <- split_lines(text)) {
       line match {
-        case Session_Finished(name,
+        case Session_Finished1(name,
             Value.Int(e1), Value.Int(e2), Value.Int(e3),
             Value.Int(c1), Value.Int(c2), Value.Int(c3)) =>
           val elapsed = Time.hms(e1, e2, e3)
           val cpu = Time.hms(c1, c2, c3)
           finished += (name -> Timing(elapsed, cpu, Time.zero))
+        case Session_Finished2(name,
+            Value.Int(e1), Value.Int(e2), Value.Int(e3)) =>
+          val elapsed = Time.hms(e1, e2, e3)
+          finished += (name -> Timing(elapsed, Time.zero, Time.zero))
         case Session_Timing(name,
             Value.Int(t), Value.Double(e), Value.Double(c), Value.Double(g)) =>
           val elapsed = Time.seconds(e)