src/Pure/library.scala
changeset 73344 f5c147654661
parent 73339 9efdebe24c65
child 73355 ec52a1a6ed31
--- a/src/Pure/library.scala	Mon Mar 01 22:50:00 2021 +0100
+++ b/src/Pure/library.scala	Mon Mar 01 23:17:47 2021 +0100
@@ -108,7 +108,7 @@
   def first_line(source: CharSequence): String =
   {
     val lines = separated_chunks(_ == '\n', source)
-    if (lines.hasNext) lines.next.toString
+    if (lines.hasNext) lines.next().toString
     else ""
   }