# HG changeset patch
# User wenzelm
# Date 1621253233 -7200
# Node ID e7deaadc5eab48431b3ef84e14f6bf7cb41a0305
# Parent  d95d34efbe6f79c35c77fd1dc69cd53dff213a03
tuned;

diff -r d95d34efbe6f -r e7deaadc5eab src/Pure/Admin/build_csdp.scala
--- 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"))
     }