# HG changeset patch
# User wenzelm
# Date 1713273295 -7200
# Node ID 47f671888a371da009b594bcb22f78f3336921a3
# Parent  0323cd9fcab977cb5033b58d77f28a4032ac5fd2
tuned;

diff -r 0323cd9fcab9 -r 47f671888a37 src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Tue Apr 16 15:11:13 2024 +0200
+++ b/src/Pure/Tools/update.scala	Tue Apr 16 15:14:55 2024 +0200
@@ -217,13 +217,13 @@
                 sessions = sessions),
               base_logics = base_logics,
               progress = progress,
-              build_heap,
-              clean_build,
+              build_heap = build_heap,
+              clean_build = clean_build,
               dirs = dirs,
               select_dirs = select_dirs,
               numa_shuffling = Host.numa_check(progress, numa_shuffling),
               max_jobs = max_jobs,
-              fresh_build,
+              fresh_build = fresh_build,
               no_build = no_build)
           }