src/Pure/Admin/build_csdp.scala

--- a/src/Pure/Admin/build_csdp.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Admin/build_csdp.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -31,7 +31,7 @@
       def change_line(line: String, entry: (String, String)): String =
         line.replaceAll(entry._1 + "=.*", entry._1 + "=" + entry._2)
       File.change(path, s =>
-        split_lines(s).map(line => (line /: changed)(change_line)).mkString("\n"))
+        split_lines(s).map(line => changed.foldLeft(line)(change_line)).mkString("\n"))
     }
   }