# HG changeset patch
# User wenzelm
# Date 1677705744 -3600
# Node ID ed292479eaa9858bdc5cbeccc0040be8dba5dfe5
# Parent  e27bc79572978bb1715db65260febde28946a100
tuned;

diff -r e27bc7957297 -r ed292479eaa9 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 01 22:06:49 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 01 22:22:24 2023 +0100
@@ -185,9 +185,6 @@
       val entry = name -> Build_Process.Result(process_result, output_shasum, node_info, current)
       copy(results = results + entry)
     }
-
-    def get_results(names: List[String]): List[Build_Process.Result] =
-      names.map(results.apply)
   }
 
 
@@ -557,7 +554,8 @@
     else None
 
   protected def start_session(state: Build_Process.State, session_name: String): Build_Process.State = {
-    val ancestor_results = state.get_results(build_context.sessions(session_name).ancestors)
+    val ancestor_results =
+      for (a <- build_context.sessions(session_name).ancestors) yield state.results(a)
 
     val input_shasum =
       if (ancestor_results.isEmpty) {