# HG changeset patch # User wenzelm # Date 1476171479 -7200 # Node ID cf0c8c5782aff2c41c7ed1b8e1f1af7cc733cd0c # Parent e9b3d9c1bc5aa1a66aa2231e029891c0a7106f87 eliminated extra trim_line: Process_Result.out/err are based on cat_lines, without trailing newline; diff -r e9b3d9c1bc5a -r cf0c8c5782af src/Pure/General/mercurial.scala --- a/src/Pure/General/mercurial.scala Tue Oct 11 09:32:56 2016 +0200 +++ b/src/Pure/General/mercurial.scala Tue Oct 11 09:37:59 2016 +0200 @@ -47,7 +47,7 @@ command("manifest " + options + opt_rev(rev)).check.out_lines def log(rev: String = "", template: String = "", options: String = ""): String = - Library.trim_line(command("log " + options + opt_rev(rev) + opt_template(template)).check.out) + command("log " + options + opt_rev(rev) + opt_template(template)).check.out def pull(remote: String = "", rev: String = "", options: String = ""): Unit = command("pull " + options + opt_rev(rev) + optional(remote)).check 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) } diff -r e9b3d9c1bc5a -r cf0c8c5782af src/Pure/Tools/build_history.scala --- a/src/Pure/Tools/build_history.scala Tue Oct 11 09:32:56 2016 +0200 +++ b/src/Pure/Tools/build_history.scala Tue Oct 11 09:37:59 2016 +0200 @@ -217,7 +217,7 @@ /* main */ val build_history_date = Date.now() - val build_host = Library.trim_line(Isabelle_System.bash("hostname").check.out) + val build_host = Isabelle_System.bash("hostname").check.out var first_build = true for (threads <- threads_list) yield