--- 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,