# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1724239999 -7200
# Node ID 834849b5591063802d00f221551f10b8d4730758
# Parent  be4c1fbccfe884415ea2f24742536422fa125b98
remove terminated jobs, even if futures do not complete;

diff -r be4c1fbccfe8 -r 834849b55910 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Tue Aug 20 17:28:51 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Wed Aug 21 13:33:19 2024 +0200
@@ -811,7 +811,7 @@
       }
 
       def update: (State, Map[String, Process_Result]) = {
-        val finished =
+        val finished0 =
           for ((name, future) <- result_futures if future.is_finished)
           yield name ->
             (future.join_result match {
@@ -819,11 +819,20 @@
               case Exn.Exn(exn) => Process_Result(Process_Result.RC.interrupt).error(exn.getMessage)
             })
 
+        val (terminated, cancelling_until1) =
+          cancelling_until
+            .filterNot((name, _) => finished0.contains(name))
+            .partition((name, _) => do_terminate(name))
+
+        val finished =
+          finished0 ++
+            terminated.map((name, _) => name -> Process_Result(Process_Result.RC.timeout))
+
         val state1 =
           copy(
             process_futures.filterNot((name, _) => finished.contains(name)),
             result_futures.filterNot((name, _) => finished.contains(name)),
-            cancelling_until.filterNot((name, _) => finished.contains(name) || do_terminate(name)))
+            cancelling_until1)
         (state1, finished)
       }