more robust: process stdout on Windows may contain CR;
authorwenzelm
Wed, 01 Apr 2020 22:07:57 +0200
changeset 71653 6f7a54954f19
parent 71652 721f143a679b
child 71654 0aef1812ae3a
more robust: process stdout on Windows may contain CR;
src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Wed Apr 01 21:43:22 2020 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed Apr 01 22:07:57 2020 +0200
@@ -110,10 +110,10 @@
     }
 
     def apply(name: String, lines: List[String]): Log_File =
-      new Log_File(plain_name(name), lines)
+      new Log_File(plain_name(name), lines.map(Library.trim_line))
 
     def apply(name: String, text: String): Log_File =
-      Log_File(name, Library.trim_split_lines(text))
+      new Log_File(plain_name(name), Library.trim_split_lines(text))
 
     def apply(file: JFile): Log_File =
     {