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