src/Pure/Admin/build_csdp.scala

--- a/src/Pure/Admin/build_csdp.scala	Thu Mar 03 17:15:30 2022 +0100
+++ b/src/Pure/Admin/build_csdp.scala	Thu Mar 03 17:21:57 2022 +0100
@@ -30,9 +30,7 @@
     {
       def change_line(line: String, p: (String, String)): String =
         line.replaceAll(p._1 + "=.*", Properties.Eq(p))
-      File.change(path) { s =>
-        split_lines(s).map(line => changed.foldLeft(line)(change_line)).mkString("\n")
-      }
+      File.change_lines(path) { _.map(line => changed.foldLeft(line)(change_line)) }
     }
   }