| changeset 77007 | 19a7046f90f9 |
| parent 76788 | ce44e714d573 |
| child 77367 | d27d1224c67f |
--- a/src/Pure/library.scala Wed Jan 18 16:04:51 2023 +0100 +++ b/src/Pure/library.scala Wed Jan 18 16:15:41 2023 +0100 @@ -94,6 +94,8 @@ /* lines */ + def count_newlines(str: String): Int = str.count(_ == '\n') + def terminate_lines(lines: IterableOnce[String]): String = { val it = lines.iterator if (it.isEmpty) "" else it.mkString("", "\n", "\n")