--- 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)
}