proper treatment of empty lines (amending 08f89f0e8a62);

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