diff -r e942eedd9229 -r 6d48d6ba58df src/Pure/Tools/build_job.scala --- a/src/Pure/Tools/build_job.scala Tue Sep 07 17:07:28 2021 +0200 +++ b/src/Pure/Tools/build_job.scala Tue Sep 07 17:13:34 2021 +0200 @@ -503,14 +503,16 @@ build_errors match { case Exn.Res(build_errs) => val errs = build_errs ::: document_errors - if (errs.isEmpty) result - else { + if (errs.nonEmpty) { result.error_rc.output( errs.flatMap(s => split_lines(Output.error_message_text(s))) ::: errs.map(Protocol.Error_Message_Marker.apply)) } + else if (progress.stopped && result.ok) result.copy(rc = Process_Result.interrupt_rc) + else result case Exn.Exn(Exn.Interrupt()) => - if (result.ok) result.copy(rc = Process_Result.interrupt_rc) else result + if (result.ok) result.copy(rc = Process_Result.interrupt_rc) + else result case Exn.Exn(exn) => throw exn } }