# HG changeset patch
# User wenzelm
# Date 1606142075 -3600
# Node ID 0201ae3675189773eb9e7aa42a7f8b0235c38c3a
# Parent  22aeec526ffda2e49137cd2ed6236d696c5f5b34
unused;

diff -r 22aeec526ffd -r 0201ae367518 src/Pure/Tools/build.scala
--- 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)
                 }
diff -r 22aeec526ffd -r 0201ae367518 src/Pure/Tools/build_job.scala
--- 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])