--- a/src/Pure/Tools/update.scala Thu Mar 16 17:12:06 2023 +0100
+++ b/src/Pure/Tools/update.scala Fri Mar 17 12:10:14 2023 +0100
@@ -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)