eliminated extra trim_line: Process_Result.out/err are based on cat_lines, without trailing newline;
--- 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
--- 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)
}
--- 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