more robust: progress.stopped means that build has failed;
authorwenzelm
Tue, 07 Sep 2021 17:13:34 +0200
changeset 74259 6d48d6ba58df
parent 74258 e942eedd9229
child 74260 bb37fb85d82c
more robust: progress.stopped means that build has failed;
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
       }
     }