changeset 75859 | 7164f537370f |
parent 75709 | a068fb7346ef |
child 76788 | ce44e714d573 |
--- a/src/Pure/library.scala Sun Aug 14 11:20:10 2022 +0200 +++ b/src/Pure/library.scala Sun Aug 14 11:39:28 2022 +0200 @@ -94,8 +94,10 @@ /* lines */ - def terminate_lines(lines: IterableOnce[String]): String = - lines.iterator.mkString("", "\n", "\n") + def terminate_lines(lines: IterableOnce[String]): String = { + val it = lines.iterator + if (it.isEmpty) "" else it.mkString("", "\n", "\n") + } def cat_lines(lines: IterableOnce[String]): String = lines.iterator.mkString("\n")