--- 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 =