# HG changeset patch
# User wenzelm
# Date 1606405900 -3600
# Node ID ec6a27bbdab86d158dffceebd51a1113597c312c
# Parent  27d9aa2a401046fc1b12903fa7c495d6d4ce192b
proper return code for more errors (amending d892f6d66402);

diff -r 27d9aa2a4010 -r ec6a27bbdab8 src/Pure/System/process_result.scala
--- a/src/Pure/System/process_result.scala	Thu Nov 26 16:19:55 2020 +0100
+++ b/src/Pure/System/process_result.scala	Thu Nov 26 16:51:40 2020 +0100
@@ -53,6 +53,9 @@
 
   def error_rc: Process_Result = if (interrupted) this else copy(rc = rc max 1)
 
+  def errors_rc(errs: List[String]): Process_Result =
+    if (errs.isEmpty) this else errors(errs).error_rc
+
   def check_rc(pred: Int => Boolean): Process_Result =
     if (pred(rc)) this
     else if (interrupted) throw Exn.Interrupt()
diff -r 27d9aa2a4010 -r ec6a27bbdab8 src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Thu Nov 26 16:19:55 2020 +0100
+++ b/src/Pure/Tools/build_job.scala	Thu Nov 26 16:51:40 2020 +0100
@@ -263,10 +263,9 @@
             task_statistics.toList.map(Protocol.Task_Statistics_Marker.apply) :::
             document_output
 
-        val more_errors =
-          Library.trim_line(stderr.toString) :: export_errors ::: document_errors
-
-        process_result.output(more_output).errors(more_errors)
+        process_result.output(more_output)
+          .error(Library.trim_line(stderr.toString))
+          .errors_rc(export_errors ::: document_errors)
       }
 
       build_errors match {