proper synchronized;
authorFabian Huch <huch@in.tum.de>
Tue, 25 Jun 2024 13:44:20 +0200
changeset 80405 661a226bb49a
parent 80404 f34e62eda167
child 80406 d85ad13d8cf3
proper synchronized;
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 = {