--- a/src/Pure/Tools/build_process.scala Wed Mar 01 15:45:58 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Wed Mar 01 16:01:01 2023 +0100
@@ -597,7 +597,15 @@
make_result(session_name, false, output_heap, Process_Result.error)
}
}
- else if (ancestor_results.forall(_.ok) && !progress.stopped) {
+ else if (!ancestor_results.forall(_.ok) || progress.stopped) {
+ progress.echo(session_name + " CANCELLED")
+ synchronized {
+ _state = _state.
+ remove_pending(session_name).
+ make_result(session_name, false, output_heap, Process_Result.undefined)
+ }
+ }
+ else {
progress.echo((if (do_store) "Building " else "Running ") + session_name + " ...")
store.clean_output(session_name)
@@ -628,14 +636,6 @@
}
job.start()
}
- else {
- progress.echo(session_name + " CANCELLED")
- synchronized {
- _state = _state.
- remove_pending(session_name).
- make_result(session_name, false, output_heap, Process_Result.undefined)
- }
- }
}