# HG changeset patch
# User wenzelm
# Date 1604763410 -3600
# Node ID 7abd365058e9f47cd9250555cd6fec54df9260e8
# Parent  653ac845b4662735bb900509bb69bfc7b74b4c2d
unused;

diff -r 653ac845b466 -r 7abd365058e9 src/Pure/System/process_result.scala
--- 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
 }