author | wenzelm |
Sat, 07 Nov 2020 16:36:50 +0100 | |
changeset 72556 | 7abd365058e9 |
parent 72555 | 653ac845b466 |
child 72557 | 6345cce0e576 |
--- a/src/Pure/System/process_result.scala Fri Nov 06 20:51:07 2020 +0100 +++ b/src/Pure/System/process_result.scala Sat Nov 07 16:36:50 2020 +0100 @@ -76,7 +76,4 @@ Output.writeln(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 }