tuned;

--- a/src/Pure/Tools/build.scala	Sat Feb 11 21:55:46 2023 +0100
+++ b/src/Pure/Tools/build.scala	Sat Feb 11 22:02:39 2023 +0100
@@ -38,15 +38,15 @@
     ): Queue = {
       val context = Build_Process.Context(sessions_structure, store, progress = progress)
       val build_graph = sessions_structure.build_graph
-      val sessions = SortedSet.from(build_graph.keys)(context.ordering)
-      new Queue(context, build_graph, sessions)
+      val build_order = SortedSet.from(build_graph.keys)(context.ordering)
+      new Queue(context, build_graph, build_order)
     }
   }
 
   private class Queue(
     context: Build_Process.Context,
     build_graph: Graph[String, Sessions.Info],
-    order: SortedSet[String]
+    build_order: SortedSet[String]
   ) {
     def old_command_timings(name: String): List[Properties.T] =
       context(name).old_command_timings
@@ -56,10 +56,10 @@
     def is_empty: Boolean = build_graph.is_empty
 
     def - (name: String): Queue =
-      new Queue(context, build_graph.del_node(name), order - name)
+      new Queue(context, build_graph.del_node(name), build_order - name)
 
     def dequeue(skip: String => Boolean): Option[String] =
-      order.iterator.dropWhile(name => skip(name) || !build_graph.is_minimal(name))
+      build_order.iterator.dropWhile(name => skip(name) || !build_graph.is_minimal(name))
         .nextOption()
   }