# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1722945250 -7200
# Node ID 6a996ad11af29eeb5be95979ad912fdfae29b2d5
# Parent  11b8f2e4c3d2e1971c6e39f51e9b93dacaea9e2b
build_manager: log message when job is cancelled;

diff -r 11b8f2e4c3d2 -r 6a996ad11af2 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Tue Aug 06 12:31:42 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Tue Aug 06 13:54:10 2024 +0200
@@ -933,8 +933,15 @@
           echo(job.name + ": " + timeout_msg)
         }
 
-        val cancelled = for (name <- state.running if _state.running(name).cancelled) yield name
-        state.cancel(cancelled)
+        val cancelled =
+          for {
+            name <- state.running
+            job = _state.running(name)
+            if job.cancelled
+          } yield job
+
+        cancelled.foreach(job => store.report(job.kind, job.id).progress.echo("Cancelling ..."))
+        state.cancel(cancelled.map(_.name))
       }
 
     private def finish_job(name: String, process_result: Process_Result): Unit =