# HG changeset patch
# User wenzelm
# Date 1678741726 -3600
# Node ID d5344cc1fae71a1d6bad6878247c86742a129af3
# Parent  a4266d54ec35c930af01aa44a22387675c988e30
avoid too many synchronized_database;

diff -r a4266d54ec35 -r d5344cc1fae7 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Mon Mar 13 21:43:55 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Mon Mar 13 22:08:46 2023 +0100
@@ -1061,12 +1061,12 @@
 
       try {
         while (!finished()) {
-          if (progress.stopped) synchronized_database { _state.stop_running() }
+          synchronized_database {
+            if (progress.stopped) _state.stop_running()
 
-          for (build <- synchronized_database { _state.finished_running() }) {
-            val job_name = build.job_name
-            val (process_result, output_shasum) = build.join
-            synchronized_database {
+            for (build <- _state.finished_running()) {
+              val job_name = build.job_name
+              val (process_result, output_shasum) = build.join
               _state = _state.
                 remove_pending(job_name).
                 remove_running(job_name).