# HG changeset patch
# User traytel
# Date 1471419992 -7200
# Node ID a2dffa971ec65e96384f972ca2fdebfdf12fb3cc
# Parent  d68d10fdec78fd5cbdb73b8916c10327c8c952d4# Parent  77323d963ca46b0fac3204c89e9366631288c93c
merged

diff -r d68d10fdec78 -r a2dffa971ec6 src/Pure/Tools/build_stats.scala
--- a/src/Pure/Tools/build_stats.scala	Fri Mar 04 17:50:22 2016 +0100
+++ b/src/Pure/Tools/build_stats.scala	Wed Aug 17 09:46:32 2016 +0200
@@ -117,8 +117,8 @@
           val data =
             for { (t, stats) <- all_build_stats if stats.finished.isDefinedAt(session) }
             yield {
-              val finished = stats.finished(session)
-              val timing = stats.timing(session)
+              val finished = stats.finished.getOrElse(session, Timing.zero)
+              val timing = stats.timing.getOrElse(session, Timing.zero)
               List(t.toString, finished.elapsed.minutes, finished.cpu.minutes,
                 timing.elapsed.minutes, timing.cpu.minutes, timing.gc.minutes).mkString(" ")
             }