--- a/src/Pure/Admin/build_csdp.scala Mon Mar 01 20:12:09 2021 +0100
+++ b/src/Pure/Admin/build_csdp.scala Mon Mar 01 22:22:12 2021 +0100
@@ -26,7 +26,7 @@
Some(" * " + platform + ":\n" + changed.map(p => " " + p._1 + "=" + p._2)
.mkString("\n"))
- def change(path: Path)
+ def change(path: Path): Unit =
{
def change_line(line: String, entry: (String, String)): String =
line.replaceAll(entry._1 + "=.*", entry._1 + "=" + entry._2)
@@ -56,7 +56,7 @@
verbose: Boolean = false,
progress: Progress = new Progress,
target_dir: Path = Path.current,
- mingw: MinGW = MinGW.none)
+ mingw: MinGW = MinGW.none): Unit =
{
mingw.check