# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1719315860 -7200
# Node ID 661a226bb49ad0c399908d7c620822a6fc83840e
# Parent  f34e62eda1675a6968399d42691ea4e937ddbd15
proper synchronized;

diff -r f34e62eda167 -r 661a226bb49a src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Tue Jun 25 11:08:00 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Tue Jun 25 13:44:20 2024 +0200
@@ -911,8 +911,8 @@
     progress: Progress
   ) extends Loop_Process[Date]("Timer", store, progress) {
 
-    private def add_tasks(previous: Date, next: Date): Unit =
-      for (ci_job <-ci_jobs)
+    private def add_tasks(previous: Date, next: Date): Unit = synchronized_database("add_tasks") {
+      for (ci_job <- ci_jobs)
         ci_job.trigger match {
           case isabelle.CI_Build.Timed(in_interval) if in_interval(previous, next) =>
             val task = Task(CI_Build(ci_job), ci_job.hosts.hosts_spec, isabelle_rev = "default")
@@ -920,6 +920,7 @@
             _state = _state.add_pending(task)
           case _ =>
         }
+    }
 
     def init: Date = Date.now()
     def loop_body(previous: Date): Date = {