proper cat_lines: avoid last "\n";
authorwenzelm
Fri, 16 Jul 2021 11:32:32 +0200
changeset 74009 10abe3049bec
parent 74004 5c8a0580d513
child 74010 4f60db51a263
proper cat_lines: avoid last "\n";
src/Tools/Setup/isabelle/setup/Library.java
--- a/src/Tools/Setup/isabelle/setup/Library.java	Thu Jul 15 22:51:49 2021 +0200
+++ b/src/Tools/Setup/isabelle/setup/Library.java	Fri Jul 16 11:32:32 2021 +0200
@@ -33,13 +33,9 @@
     {
         if (str.isEmpty()) { return str; }
         else {
-            StringBuilder result = new StringBuilder();
-            for (String s : split_lines(str)) {
-                result.append(prfx);
-                result.append(s);
-                result.append('\n');
-            }
-            return result.toString();
+            List<String> lines = new LinkedList<String>();
+            for (String line : split_lines(str)) { lines.add(prfx + line); }
+            return cat_lines(lines);
         }
     }