# HG changeset patch
# User wenzelm
# Date 1529766359 -7200
# Node ID 3d710aa238463eedd826aec928f9d67f23ee0f63
# Parent  6984a55f3cbac0efe49e56ab470a3c0679b0d5c8
tuned;

diff -r 6984a55f3cba -r 3d710aa23846 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Jun 23 14:23:53 2018 +0200
+++ b/src/Pure/Tools/build.scala	Sat Jun 23 17:05:59 2018 +0200
@@ -67,14 +67,18 @@
     def make_session_timing(sessions: Sessions.Structure, timing: Map[String, Double])
       : Map[String, Double] =
     {
+      val maximals = sessions.build_graph.maximals.toSet
       def desc_timing(name: String): Double =
       {
-        val g = sessions.build_graph.restrict(sessions.build_descendants(List(name)).toSet)
-        (0.0 :: g.maximals.flatMap(desc => {
-          val ps = g.all_preds(List(desc))
-          if (ps.exists(p => timing.get(p).isEmpty)) None
-          else Some(ps.map(timing(_)).sum)
-        })).max
+        if (maximals.contains(name)) timing(name)
+        else {
+          val g = sessions.build_graph.restrict(sessions.build_descendants(List(name)).toSet)
+          (0.0 :: g.maximals.flatMap(desc => {
+            val ps = g.all_preds(List(desc))
+            if (ps.exists(p => timing.get(p).isEmpty)) None
+            else Some(ps.map(timing(_)).sum)
+          })).max
+        }
       }
       timing.keySet.iterator.map(name => (name -> desc_timing(name))).toMap.withDefaultValue(0.0)
     }