eliminated extra trim_line: Process_Result.out/err are based on cat_lines, without trailing newline;
authorwenzelm
Tue, 11 Oct 2016 09:37:59 +0200
changeset 64138 cf0c8c5782af
parent 64137 e9b3d9c1bc5a
child 64139 387c811cad6a
eliminated extra trim_line: Process_Result.out/err are based on cat_lines, without trailing newline;
src/Pure/General/mercurial.scala
src/Pure/System/process_result.scala
src/Pure/Tools/build_history.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
--- 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