# HG changeset patch
# User wenzelm
# Date 1673726486 -3600
# Node ID 4307b5de7009be4a0a2d44e2360675193f026e02
# Parent  e5dafe9e120f786e48578de255c255eb1e8efcc8
tuned whitespace;

diff -r e5dafe9e120f -r 4307b5de7009 src/Pure/Tools/update.scala
--- a/src/Pure/Tools/update.scala	Sat Jan 14 20:42:48 2023 +0100
+++ b/src/Pure/Tools/update.scala	Sat Jan 14 21:01:26 2023 +0100
@@ -73,7 +73,7 @@
     val build_results =
       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,
+        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