# HG changeset patch
# User wenzelm
# Date 1622840318 -7200
# Node ID 451fc6be6c5bc939c8b5e58dc43a1392b4642f43
# Parent  2141d6c83511db273f1b278d4169e48cc88cb070
unused;

diff -r 2141d6c83511 -r 451fc6be6c5b src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Jun 04 22:50:32 2021 +0200
+++ b/src/Pure/Tools/build.scala	Fri Jun 04 22:58:38 2021 +0200
@@ -425,7 +425,7 @@
                   val numa_node = numa_nodes.next(used_node)
                   val job =
                     new Build_Job(progress, session_name, info, deps, store, do_store,
-                      verbose, log, numa_node, queue.command_timings(session_name))
+                      log, numa_node, queue.command_timings(session_name))
                   loop(pending, running + (session_name -> (ancestor_heaps, job)), results)
                 }
                 else {
diff -r 2141d6c83511 -r 451fc6be6c5b src/Pure/Tools/build_job.scala
--- a/src/Pure/Tools/build_job.scala	Fri Jun 04 22:50:32 2021 +0200
+++ b/src/Pure/Tools/build_job.scala	Fri Jun 04 22:58:38 2021 +0200
@@ -202,7 +202,6 @@
   deps: Sessions.Deps,
   store: Sessions.Store,
   do_store: Boolean,
-  verbose: Boolean,
   log: Logger,
   val numa_node: Option[Int],
   command_timings0: List[Properties.T])