--- a/src/Pure/Admin/build_csdp.scala Mon May 17 13:37:47 2021 +0200
+++ b/src/Pure/Admin/build_csdp.scala Mon May 17 13:40:01 2021 +0200
@@ -23,13 +23,13 @@
def print: Option[String] =
if (changed.isEmpty) None
else
- Some(" * " + platform + ":\n" + changed.map(p => " " + p._1 + "=" + p._2)
+ Some(" * " + platform + ":\n" + changed.map(p => " " + Properties.Eq(p))
.mkString("\n"))
def change(path: Path): Unit =
{
def change_line(line: String, entry: (String, String)): String =
- line.replaceAll(entry._1 + "=.*", entry._1 + "=" + entry._2)
+ line.replaceAll(entry._1 + "=.*", Properties.Eq(entry))
File.change(path, s =>
split_lines(s).map(line => changed.foldLeft(line)(change_line)).mkString("\n"))
}