# HG changeset patch # User wenzelm # Date 1606304048 -3600 # Node ID 6f83f7892317ad9ffb08dd14d79304b5165e57a9 # Parent e16f85e3c288349d08bb116a0ef60f0bed1d4cc8 clarified: more uniform; diff -r e16f85e3c288 -r 6f83f7892317 src/Pure/General/file.scala --- a/src/Pure/General/file.scala Tue Nov 24 16:49:42 2020 +0100 +++ b/src/Pure/General/file.scala Wed Nov 25 12:34:08 2020 +0100 @@ -222,7 +222,7 @@ val line = try { reader.readLine} catch { case _: IOException => null } - Option(line) + Option(line).map(Library.trim_line) } def read_lines(reader: BufferedReader, progress: String => Unit): List[String] =