# HG changeset patch
# User wenzelm
# Date 1590485133 -7200
# Node ID 7a39036d5a19c436757b38be54e594309d9c7a2f
# Parent  ab21876c30c1d5b78e3b8c8a0e5bbf652e49a3f4
tuned;

diff -r ab21876c30c1 -r 7a39036d5a19 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue May 26 11:17:10 2020 +0200
+++ b/src/Pure/Tools/build.scala	Tue May 26 11:25:33 2020 +0200
@@ -76,7 +76,7 @@
           val g = sessions_structure.build_graph.restrict(descendants)
           (0.0 :: g.maximals.flatMap(desc => {
             val ps = g.all_preds(List(desc))
-            if (ps.exists(p => timing.get(p).isEmpty)) None
+            if (ps.exists(p => !timing.isDefinedAt(p))) None
             else Some(ps.map(timing(_)).sum)
           })).max
         }
@@ -162,7 +162,7 @@
     val numa_node: Option[Int],
     command_timings: List[Properties.T])
   {
-    val options = NUMA.policy_options(info.options, numa_node)
+    val options: Options = NUMA.policy_options(info.options, numa_node)
 
     private val sessions_structure = deps.sessions_structure