# HG changeset patch
# User wenzelm
# Date 1709667667 -3600
# Node ID 3e5a06add554e945233232d6033cf0f2d963f7ba
# Parent  6fadff9e849a1ef3309df359fd6e383b9993977d
clarified signature;

diff -r 6fadff9e849a -r 3e5a06add554 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Tue Mar 05 20:25:02 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Tue Mar 05 20:41:07 2024 +0100
@@ -224,9 +224,6 @@
 
     def is_running(name: String): Boolean = running.isDefinedAt(name)
 
-    def stop_running(): Unit =
-      for (job <- running.valuesIterator; build <- job.build) build.cancel()
-
     def build_running: List[Build_Job] =
       List.from(for (job <- running.valuesIterator; build <- job.build) yield build)
 
@@ -1183,7 +1180,7 @@
       try {
         while (!finished()) {
           synchronized_database("Build_Process.main") {
-            if (progress.stopped) _state.stop_running()
+            if (progress.stopped) _state.build_running.foreach(_.cancel())
             main_unsynchronized()
           }
           sleep()