# HG changeset patch
# User wenzelm
# Date 1457386651 -3600
# Node ID d2e0d626fb964b88b166c23912a344e148194ffe
# Parent  53603d1aad5fb25c37f8ea6b37bc61f370740bfd
tuned signature;

diff -r 53603d1aad5f -r d2e0d626fb96 src/Pure/General/output.scala
--- a/src/Pure/General/output.scala	Mon Mar 07 22:36:44 2016 +0100
+++ b/src/Pure/General/output.scala	Mon Mar 07 22:37:31 2016 +0100
@@ -18,7 +18,27 @@
   def warning_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
   def error_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
 
-  def writeln(msg: String) { if (msg != "") Console.err.println(writeln_text(msg)) }
-  def warning(msg: String) { if (msg != "") Console.err.println(warning_text(msg)) }
-  def error_message(msg: String) { if (msg != "") Console.err.println(error_text(msg)) }
+  def writeln(msg: String, stdout: Boolean = false)
+  {
+    if (msg != "") {
+      if (stdout) Console.println(writeln_text(msg))
+      else Console.err.println(writeln_text(msg))
+    }
+  }
+
+  def warning(msg: String, stdout: Boolean = false)
+  {
+    if (msg != "") {
+      if (stdout) Console.println(warning_text(msg))
+      else Console.err.println(warning_text(msg))
+    }
+  }
+
+  def error_message(msg: String, stdout: Boolean = false)
+  {
+    if (msg != "") {
+      if (stdout) Console.println(error_text(msg))
+      else Console.err.println(error_text(msg))
+    }
+  }
 }
diff -r 53603d1aad5f -r d2e0d626fb96 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)
+  }
 }