# HG changeset patch
# User wenzelm
# Date 1660469968 -7200
# Node ID 7164f537370f3595ae8351fbb76a55cef5fba86e
# Parent  657b2de27454d146f2ede9826bbf59caac346949
proper treatment of empty lines (amending 08f89f0e8a62);

diff -r 657b2de27454 -r 7164f537370f src/Pure/library.scala
--- 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")