remove schedule outdated limit: delay is sufficient;
authorFabian Huch <huch@in.tum.de>
Sat, 16 Mar 2024 14:43:48 +0100
changeset 79912 fe96a842f065
parent 79911 cb06884f1040
child 79913 82bddaf3bd33
remove schedule outdated limit: delay is sufficient;
etc/options
src/Pure/Build/build_schedule.scala
--- 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 {