src/Pure/System/process_result.scala

--- a/src/Pure/System/process_result.scala	Mon Mar 07 22:36:44 2016 +0100
+++ b/src/Pure/System/process_result.scala	Mon Mar 07 22:37:31 2016 +0100
@@ -32,4 +32,11 @@
     Output.writeln(Library.trim_line(out))
     copy(out_lines = Nil, err_lines = Nil)
   }
+
+  def print_stdout: Process_Result =
+  {
+    Output.warning(Library.trim_line(err), stdout = true)
+    Output.writeln(Library.trim_line(out), stdout = true)
+    copy(out_lines = Nil, err_lines = Nil)
+  }
 }