# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1719316425 -7200
# Node ID d85ad13d8cf32fe081614388f5ca0494c7771675
# Parent  661a226bb49ad0c399908d7c620822a6fc83840e
extra timer delay, to limit db transactions;

diff -r 661a226bb49a -r d85ad13d8cf3 etc/options
--- a/etc/options	Tue Jun 25 13:44:20 2024 +0200
+++ b/etc/options	Tue Jun 25 13:53:45 2024 +0200
@@ -251,6 +251,9 @@
 option build_manager_poll_delay : real = 60.0
   -- "delay build manager poll loop"
 
+option build_manager_timer_delay : real = 10.0
+  -- "delay build manager timer loop"
+
 option build_manager_ci_jobs : string = "benchmark"
   -- "ci jobs that should be executed on repository changes"
 
diff -r 661a226bb49a -r d85ad13d8cf3 src/Pure/Build/build_manager.scala
--- 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 {