# HG changeset patch # User Fabian Huch # Date 1700858992 -3600 # Node ID 1a9f3806987ddfb513a41b912e04c24adcf8aedb # Parent ff7d48e776abd1baa399cd5a3783336bc69c0bd2 proper split; diff -r ff7d48e776ab -r 1a9f3806987d src/Pure/Tools/build_schedule.scala --- a/src/Pure/Tools/build_schedule.scala Fri Nov 24 17:52:04 2023 +0100 +++ b/src/Pure/Tools/build_schedule.scala Fri Nov 24 21:49:52 2023 +0100 @@ -95,8 +95,8 @@ } else { // Piecewise linear val (p0, p1) = - if (entries.head._1 <= threads && threads <= entries.last._1) { - val split = entries.partition(_._1 <= threads) + if (entries.head._1 < threads && threads < entries.last._1) { + val split = entries.partition(_._1 < threads) (split._1.last, split._2.head) } else { val piece = if (threads < entries.head._1) entries.take(2) else entries.takeRight(2)