# HG changeset patch
# User wenzelm
# Date 1673006948 -3600
# Node ID cd8f6634db17c736ec887b0d2f0b6f86025d38c7
# Parent  da13da82f6f95c94da6664a05891c6f5636be554
proper build parameters (amending d858e6f15da3);

diff -r da13da82f6f9 -r cd8f6634db17 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