src/Pure/System/process_result.scala

--- a/src/Pure/System/process_result.scala	Mon Jul 06 16:52:48 2020 +0200
+++ b/src/Pure/System/process_result.scala	Wed Jul 08 14:43:02 2020 +0200
@@ -42,7 +42,8 @@
     copy(out_lines = out_lines ::: outs.flatMap(split_lines))
   def errors(errs: List[String]): Process_Result =
     copy(err_lines = err_lines ::: errs.flatMap(split_lines))
-  def error(err: String): Process_Result = errors(List(err))
+  def error(err: String): Process_Result =
+    if (err.isEmpty) this else errors(List(err))
 
   def was_timeout: Process_Result = copy(rc = 1, timeout = true)