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