# HG changeset patch # User wenzelm # Date 1585771677 -7200 # Node ID 6f7a54954f19a5e5e83ad52c2b0aacd1fabf2376 # Parent 721f143a679b88e0567f2dab7cbca68ab2b3ea6c more robust: process stdout on Windows may contain CR; diff -r 721f143a679b -r 6f7a54954f19 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 = {