# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# 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)