| changeset 64024 | 3dd92c391eca |
| parent 62569 | 5db10482f4cf |
| child 64138 | cf0c8c5782af |
--- a/src/Pure/System/process_result.scala Mon Oct 03 18:54:59 2016 +0200 +++ b/src/Pure/System/process_result.scala Mon Oct 03 20:09:50 2016 +0200 @@ -40,4 +40,7 @@ Output.writeln(Library.trim_line(out), stdout = true) copy(out_lines = Nil, err_lines = Nil) } + + def print_if(b: Boolean): Process_Result = if (b) print else this + def print_stdout_if(b: Boolean): Process_Result = if (b) print_stdout else this }