build_manager: log message when job is cancelled;
authorFabian Huch <huch@in.tum.de>
Tue, 06 Aug 2024 13:54:10 +0200
changeset 80644 6a996ad11af2
parent 80643 11b8f2e4c3d2
child 80645 a1dce0cc6c26
build_manager: log message when job is cancelled;
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 =