--- a/src/Pure/System/process_result.scala Sun May 06 22:15:52 2018 +0200
+++ b/src/Pure/System/process_result.scala Sun May 06 23:01:45 2018 +0200
@@ -15,7 +15,8 @@
{
def out: String = cat_lines(out_lines)
def err: String = cat_lines(err_lines)
- def error(s: String): Process_Result = copy(err_lines = err_lines ::: List(s))
+ def errors(errs: List[String]): Process_Result = copy(err_lines = err_lines ::: errs)
+ def error(err: String): Process_Result = errors(List(err))
def was_timeout: Process_Result = copy(rc = 1, timeout = true)