# HG changeset patch
# User wenzelm
# Date 1691659751 -7200
# Node ID a7dab3b8ebfe2b671e82aeab474f5752ca98d5cb
# Parent  964de51dd2e4780b475ccae70a4afc2460728868
clarified synchronized regions: avoid deadlock of Build_Cluster operations on other thread vs. return_code(), notably via capture() error handling;

diff -r 964de51dd2e4 -r a7dab3b8ebfe src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Wed Aug 09 14:33:59 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Thu Aug 10 11:29:11 2023 +0200
@@ -217,8 +217,10 @@
 
   private var _rc: Int = Process_Result.RC.ok
 
-  override def rc: Int = synchronized { _rc }
-  override def return_code(rc: Int): Unit = synchronized { _rc = Process_Result.RC.merge(_rc, rc) }
+  override def rc: Int = _rc.synchronized { _rc }
+
+  override def return_code(rc: Int): Unit =
+    _rc.synchronized { _rc = Process_Result.RC.merge(_rc, rc) }
 
   def capture[A](host: Build_Cluster.Host, op: String)(
     e: => A,