| changeset 72693 | 0201ae367518 |
| parent 72692 | 22aeec526ffd |
| child 72728 | caa182bdab7a |
--- a/src/Pure/Tools/build.scala Mon Nov 23 15:14:58 2020 +0100 +++ b/src/Pure/Tools/build.scala Mon Nov 23 15:34:35 2020 +0100 @@ -429,7 +429,7 @@ val numa_node = numa_nodes.next(used_node) val job = - new Build_Job(progress, session_name, info, deps, store, do_store, presentation, + new Build_Job(progress, session_name, info, deps, store, do_store, verbose, numa_node, queue.command_timings(session_name)) loop(pending, running + (session_name -> (ancestor_heaps, job)), results) }