# 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] =