tuned;
authorwenzelm
Tue, 16 Apr 2024 15:14:55 +0200
changeset 80119 47f671888a37
parent 80118 0323cd9fcab9
child 80120 370ebda8bd86
tuned;
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)
           }