changeset 81882 | 2adff49492f0 |
parent 80483 | 5b539d1d3577 |
child 81884 | 058f239b860a |
--- 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 */