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 {