# HG changeset patch
# User wenzelm
# Date 1471373677 -7200
# Node ID 77323d963ca46b0fac3204c89e9366631288c93c
# Parent  b7aab1a6cf0d7af6b22e2ab5c7e544ea2178c73e
more robust;

diff -r b7aab1a6cf0d -r 77323d963ca4 src/Pure/Tools/build_stats.scala
--- a/src/Pure/Tools/build_stats.scala	Tue Aug 16 15:55:11 2016 +0200
+++ b/src/Pure/Tools/build_stats.scala	Tue Aug 16 20:54:37 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(" ")
             }