# HG changeset patch # User Fabian Huch # Date 1709832282 -3600 # Node ID 45198ea3f0b32b0e11a465dfe85e1bf80e5583a6 # Parent 1f7dcfdb3e671a537a49f2092f9227b2f144aeef parallelize schedule optimization; diff -r 1f7dcfdb3e67 -r 45198ea3f0b3 src/Pure/Build/build_schedule.scala --- 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) + } }