# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1717774812 -7200
# Node ID 3c3a9154c1072db831ec7f67603f97e6695c2dff
# Parent  17d2f775907aba5b88384885ad3cc1c0987c528a
always handle interrupted jobs;

diff -r 17d2f775907a -r 3c3a9154c107 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Fri Jun 07 15:47:19 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Fri Jun 07 17:40:12 2024 +0200
@@ -623,7 +623,12 @@
 
       def update: (State, Map[String, Process_Result]) = {
         val finished =
-          for ((name, future) <- result_futures if future.is_finished) yield name -> future.join
+          for ((name, future) <- result_futures if future.is_finished)
+          yield name ->
+            (future.join_result match {
+              case Exn.Res(result) => result
+              case Exn.Exn(_) => Process_Result(Process_Result.RC.interrupt)
+            })
 
         val process_futures1 = process_futures.filterNot((name, _) => finished.contains(name))
         val result_futures1 = result_futures.filterNot((name, _) => finished.contains(name))