src/Pure/Build/build_manager.scala
changeset 80406 d85ad13d8cf3
parent 80405 661a226bb49a
child 80407 fc26d6200560
--- a/src/Pure/Build/build_manager.scala	Tue Jun 25 13:44:20 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Tue Jun 25 13:53:45 2024 +0200
@@ -911,6 +911,8 @@
     progress: Progress
   ) extends Loop_Process[Date]("Timer", store, progress) {
 
+    override def delay = options.seconds("build_manager_timer_delay")
+    
     private def add_tasks(previous: Date, next: Date): Unit = synchronized_database("add_tasks") {
       for (ci_job <- ci_jobs)
         ci_job.trigger match {