--- 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)
}
--- a/src/Pure/Tools/build_job.scala Mon Nov 23 15:14:58 2020 +0100
+++ b/src/Pure/Tools/build_job.scala Mon Nov 23 15:34:35 2020 +0100
@@ -16,7 +16,6 @@
deps: Sessions.Deps,
store: Sessions.Store,
do_store: Boolean,
- presentation: Presentation.Context,
verbose: Boolean,
val numa_node: Option[Int],
command_timings0: List[Properties.T])