# HG changeset patch
# User wenzelm
# Date 1676980203 -3600
# Node ID e9beaaf955bfa44b7dd5762f12bdb83ad5aa3c85
# Parent  05b97b54cb3b3bfaf9e55e2ea64db58cca7943df
tuned signature;

diff -r 05b97b54cb3b -r e9beaaf955bf src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Tue Feb 21 12:48:22 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Tue Feb 21 12:50:03 2023 +0100
@@ -198,7 +198,7 @@
     def remove_running(name: String): State =
       copy(running = running - name)
 
-    def add_result(
+    def make_result(
       name: String,
       current: Boolean,
       output_heap: SHA1.Shasum,
@@ -338,7 +338,7 @@
       _state = _state.
         remove_pending(session_name).
         remove_running(session_name).
-        add_result(session_name, false, output_heap, process_result_tail)
+        make_result(session_name, false, output_heap, process_result_tail)
     }
   }
 
@@ -380,7 +380,7 @@
       synchronized {
         _state = _state.
           remove_pending(session_name).
-          add_result(session_name, true, output_heap, Process_Result.ok)
+          make_result(session_name, true, output_heap, Process_Result.ok)
       }
     }
     else if (build_context.no_build) {
@@ -388,7 +388,7 @@
       synchronized {
         _state = _state.
           remove_pending(session_name).
-          add_result(session_name, false, output_heap, Process_Result.error)
+          make_result(session_name, false, output_heap, Process_Result.error)
       }
     }
     else if (ancestor_results.forall(_.ok) && !progress.stopped) {
@@ -417,7 +417,7 @@
       synchronized {
         _state = _state.
           remove_pending(session_name).
-          add_result(session_name, false, output_heap, Process_Result.undefined)
+          make_result(session_name, false, output_heap, Process_Result.undefined)
       }
     }
   }