src/Pure/Build/build_ci.scala
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 */