# HG changeset patch
# User desharna
# Date 1709852281 -3600
# Node ID afb26a1dea714bf2b693e41ac24cd0d345f9bf60
# Parent  ba8fb71587ae42a7947172a1361f73688153fc51# Parent  45198ea3f0b32b0e11a465dfe85e1bf80e5583a6
merged

diff -r ba8fb71587ae -r afb26a1dea71 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Thu Feb 29 11:18:26 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Thu Mar 07 23:58:01 2024 +0100
@@ -601,8 +601,10 @@
   case class Optimizer(schedulers: List[Scheduler]) extends Scheduler {
     require(schedulers.nonEmpty)
 
-    def schedule(state: Build_Process.State): Schedule =
-      schedulers.map(_.schedule(state)).minBy(_.duration.ms)
+    def schedule(state: Build_Process.State): Schedule = {
+      def main(scheduler: Scheduler): Schedule = scheduler.schedule(state)
+      Par_List.map(main, schedulers).minBy(_.duration.ms)
+    }
   }