| 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 "" }