--- a/src/Pure/Build/build_schedule.scala Wed Mar 06 21:52:58 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala Thu Mar 07 18:24:42 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)
+ }
}