# HG changeset patch
# User wenzelm
# Date 1585757986 -7200
# Node ID 86f064893dac551e252769bc6a23df1b27478dfd
# Parent  07e6053ce89cc594163d0b22377e9f6a25c158ad
clarified signature: more robust;

diff -r 07e6053ce89c -r 86f064893dac src/Pure/System/process_result.scala
--- a/src/Pure/System/process_result.scala	Wed Apr 01 14:32:30 2020 +0200
+++ b/src/Pure/System/process_result.scala	Wed Apr 01 18:19:46 2020 +0200
@@ -16,8 +16,10 @@
   def out: String = cat_lines(out_lines)
   def err: String = cat_lines(err_lines)
 
-  def output(outs: List[String]): Process_Result = copy(out_lines = out_lines ::: outs)
-  def errors(errs: List[String]): Process_Result = copy(err_lines = err_lines ::: errs)
+  def output(outs: List[String]): Process_Result =
+    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 was_timeout: Process_Result = copy(rc = 1, timeout = true)