diff -r e9b3d9c1bc5a -r cf0c8c5782af src/Pure/System/process_result.scala --- 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) }