avoid too many synchronized_database;
authorwenzelm
Mon, 13 Mar 2023 22:08:46 +0100
changeset 77639 d5344cc1fae7
parent 77638 a4266d54ec35
child 77640 9ed8b85e7d67
avoid too many synchronized_database;
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).