merged

--- 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(" ")
             }