# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1737361057 -3600
# Node ID 2adff49492f07f035aec2e62db6e2b5b6de64408
# Parent  f23fc3d21873015db0752d3e105600c0232e7bf8
clarified;

diff -r f23fc3d21873 -r 2adff49492f0 src/Pure/Build/build_ci.scala
--- a/src/Pure/Build/build_ci.scala	Fri Jan 17 13:43:16 2025 +0100
+++ b/src/Pure/Build/build_ci.scala	Mon Jan 20 09:17:37 2025 +0100
@@ -79,7 +79,9 @@
       }
   }
 
-  case class Timed(in_interval: (Date, Date) => Boolean) extends Trigger
+  case class Timed(in_interval: (Date, Date) => Boolean) extends Trigger {
+    def next(before: Date, now: Date): Boolean = in_interval(before, now)
+  }
 
 
   /* build hooks */
diff -r f23fc3d21873 -r 2adff49492f0 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Fri Jan 17 13:43:16 2025 +0100
+++ b/src/Pure/Build/build_manager.scala	Mon Jan 20 09:17:37 2025 +0100
@@ -1135,7 +1135,7 @@
     private def add_tasks(previous: Date, next: Date): Unit = synchronized_database("add_tasks") {
       for (ci_job <- ci_jobs)
         ci_job.trigger match {
-          case Build_CI.Timed(in_interval) if in_interval(previous, next) =>
+          case timer: Build_CI.Timed if timer.next(previous, next) =>
             val task = CI_Build.task(ci_job)
             echo("Triggered task " + task.kind)
             _state = _state.add_pending(task)