--- 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 */
--- 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)