# HG changeset patch
# User wenzelm
# Date 1676149359 -3600
# Node ID e2d0794d0e242e1d52200048effd4454c28f5be6
# Parent  22016642d6afe1bc9cc7b31eaba67eb87b67d1e2
tuned;

diff -r 22016642d6af -r e2d0794d0e24 src/Pure/Tools/build.scala
--- 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()
   }