--- a/src/Pure/Tools/update.scala Fri Mar 17 10:42:50 2023 +0000
+++ b/src/Pure/Tools/update.scala Fri Mar 17 11:24:52 2023 +0000
@@ -75,8 +75,10 @@
/* build */
+ val build_options = options + "build_thorough"
+
val build_results =
- Build.build(options, progress = progress, dirs = dirs, select_dirs = select_dirs,
+ Build.build(build_options, progress = progress, dirs = dirs, select_dirs = select_dirs,
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, augment_options = augment_options)