diff -r aee15b076916 -r 555c95138e26 src/Pure/General/bytes.ML
--- a/src/Pure/General/bytes.ML	Wed Feb 05 21:29:13 2025 +0100
+++ b/src/Pure/General/bytes.ML	Wed Feb 05 22:54:47 2025 +0100
@@ -36,6 +36,7 @@
   val split_lines: T -> string list
   val trim_split_lines: T -> string list
   val cat_lines: string list -> T
+  val terminate_lines: string list -> T
   val read_block: int -> BinIO.instream -> string
   val read_stream: int -> BinIO.instream -> T
   val write_stream: BinIO.outstream -> T -> unit
@@ -190,6 +191,8 @@
 
 fun cat_lines lines = build (fold add (separate "\n" lines));
 
+fun terminate_lines lines = build (fold (fn line => add line #> add "\n") lines);
+
 
 (* IO *)