# HG changeset patch
# User wenzelm
# Date 1475518190 -7200
# Node ID 3dd92c391eca42e0038edcaa0c86962e977264b8
# Parent  41f7e383c19edd427d3ebaade2911827076c0de2
more operations;

diff -r 41f7e383c19e -r 3dd92c391eca src/Pure/System/process_result.scala
--- 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
 }