# HG changeset patch
# User wenzelm
# Date 1676121860 -3600
# Node ID 7c89e848bd18d74b31530edafe28d0900155f677
# Parent  dd8f8445b8a4e99c802a7eaf0416e81239fef468
tuned;

diff -r dd8f8445b8a4 -r 7c89e848bd18 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sat Feb 11 14:18:31 2023 +0100
+++ b/src/Pure/Tools/build.scala	Sat Feb 11 14:24:20 2023 +0100
@@ -57,9 +57,11 @@
       store: Sessions.Store
     ) : Queue = {
       val graph = sessions_structure.build_graph
-      val names = graph.keys
+      val sessions = graph.keys
 
-      val timings = names.map(Build_Process.Session_Timing.load(_, store, progress = progress))
+      val timings =
+        for (session <- graph.keys)
+          yield Build_Process.Session_Timing.load(session, store, progress = progress)
       val command_timings =
         timings.map(timing => timing.session -> timing.command_timings).toMap.withDefaultValue(Nil)
       val session_timing =
@@ -78,7 +80,7 @@
           }
       }
 
-      new Queue(graph, SortedSet(names: _*)(Ordering), command_timings)
+      new Queue(graph, SortedSet.from(sessions)(Ordering), command_timings)
     }
   }