# HG changeset patch # User wenzelm # Date 1475746023 -7200 # Node ID 2c5039363ea3d88fd47be5d870a28a9a09615cf3 # Parent a7352cbde7d724e710bc02f01679eb68199a5252 tuned signature; diff -r a7352cbde7d7 -r 2c5039363ea3 src/Pure/Tools/build_log.scala --- a/src/Pure/Tools/build_log.scala Thu Oct 06 11:13:12 2016 +0200 +++ b/src/Pure/Tools/build_log.scala Thu Oct 06 11:27:03 2016 +0200 @@ -24,7 +24,7 @@ new Log_File(name, lines) def apply(name: String, text: String): Log_File = - Log_File(name, split_lines(Library.trim_line(text)).map(Library.trim_line(_))) + Log_File(name, Library.trim_split_lines(text)) } class Log_File private(val name: String, val lines: List[String]) diff -r a7352cbde7d7 -r 2c5039363ea3 src/Pure/library.scala --- a/src/Pure/library.scala Thu Oct 06 11:13:12 2016 +0200 +++ b/src/Pure/library.scala Thu Oct 06 11:27:03 2016 +0200 @@ -130,6 +130,9 @@ else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1) else s + def trim_split_lines(s: String): List[String] = + split_lines(trim_line(s)).map(trim_line(_)) + /* quote */