| changeset 71631 | 3f02bc5a5a03 |
| parent 68927 | 01f46a4b22b4 |
| child 71646 | 86f064893dac |
--- a/src/Pure/System/process_result.scala Mon Mar 30 11:59:44 2020 +0200 +++ b/src/Pure/System/process_result.scala Mon Mar 30 19:39:11 2020 +0200 @@ -15,6 +15,8 @@ { 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 error(err: String): Process_Result = errors(List(err))