src/Pure/System/process_result.scala
changeset 64138 cf0c8c5782af
parent 64024 3dd92c391eca
child 64408 50bcf976f276
--- a/src/Pure/System/process_result.scala	Tue Oct 11 09:32:56 2016 +0200
+++ b/src/Pure/System/process_result.scala	Tue Oct 11 09:37:59 2016 +0200
@@ -29,15 +29,15 @@
 
   def print: Process_Result =
   {
-    Output.warning(Library.trim_line(err))
-    Output.writeln(Library.trim_line(out))
+    Output.warning(err)
+    Output.writeln(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)
+    Output.warning(err, stdout = true)
+    Output.writeln(out, stdout = true)
     copy(out_lines = Nil, err_lines = Nil)
   }