proper build parameters (amending d858e6f15da3);
authorwenzelm
Fri, 06 Jan 2023 13:09:08 +0100
changeset 76928 cd8f6634db17
parent 76927 da13da82f6f9
child 76929 c7a165287df5
proper build parameters (amending d858e6f15da3);
src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Fri Jan 06 13:06:03 2023 +0100
+++ b/src/Pure/Tools/update.scala	Fri Jan 06 13:09:08 2023 +0100
@@ -50,7 +50,8 @@
 
     val build_results =
       Build.build(options, progress = progress, dirs = dirs, select_dirs = select_dirs,
-        selection = selection, numa_shuffling = numa_shuffling, max_jobs = max_jobs,
+        selection = selection, build_heap = build_heap, clean_build = clean_build,
+        numa_shuffling = numa_shuffling, max_jobs = max_jobs,  fresh_build = fresh_build,
         no_build = no_build, verbose = verbose, augment_options = augment_options)
 
     val store = build_results.store