merged
authorwenzelm
Fri, 24 Nov 2023 22:22:41 +0100
changeset 79057 156bfa6a2836
parent 79042 1a9f3806987d (diff)
parent 79056 1f34f6394383 (current diff)
child 79058 f13390b2c1ee
merged
--- a/src/Pure/Tools/build_schedule.scala	Fri Nov 24 21:54:30 2023 +0100
+++ b/src/Pure/Tools/build_schedule.scala	Fri Nov 24 22:22:41 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)