diff -r 0093124710db -r 9016252f9470 src/Pure/Tools/build_process.scala --- 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) - } - } }