--- a/src/Pure/Admin/build_csdp.scala Mon May 17 13:48:20 2021 +0200
+++ b/src/Pure/Admin/build_csdp.scala Mon May 17 14:07:13 2021 +0200
@@ -28,8 +28,8 @@
def change(path: Path): Unit =
{
- def change_line(line: String, entry: (String, String)): String =
- line.replaceAll(entry._1 + "=.*", Properties.Eq(entry))
+ 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"))
}