tuned whitespace;
authorwenzelm
Sat, 14 Jan 2023 21:01:26 +0100
changeset 76974 4307b5de7009
parent 76973 e5dafe9e120f
child 76975 5ba8cb258e75
tuned whitespace;
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