--- a/etc/options Sat Mar 16 11:00:18 2024 +0100
+++ b/etc/options Sat Mar 16 14:43:48 2024 +0100
@@ -222,9 +222,6 @@
option build_schedule_outdated_delay : real = 300.0
-- "delay schedule generation loop"
-option build_schedule_outdated_limit : int = 20
- -- "maximum number of sessions for which schedule stays valid"
-
section "Editor Session"
--- a/src/Pure/Build/build_schedule.scala Sat Mar 16 11:00:18 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala Sat Mar 16 14:43:48 2024 +0100
@@ -517,10 +517,7 @@
def is_empty: Boolean = graph.is_empty
def is_outdated(options: Options, state: Build_Process.State): Boolean =
if (is_empty) true
- else {
- num_built(state) > options.int("build_schedule_outdated_limit") &&
- elapsed() > options.seconds("build_schedule_outdated_delay")
- }
+ else elapsed() > options.seconds("build_schedule_outdated_delay")
def next(hostname: String, state: Build_Process.State): List[String] =
for {