--- 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"
--- 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 {