--- a/src/Pure/Tools/build_cluster.scala Fri Aug 25 20:35:28 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala Sat Aug 26 13:47:03 2023 +0200
@@ -226,12 +226,12 @@
/* cumulative return code */
- private var _rc: Int = Process_Result.RC.ok
+ private val _rc = Synchronized(Process_Result.RC.ok)
- override def rc: Int = _rc.synchronized { _rc }
+ override def rc: Int = _rc.value
override def return_code(rc: Int): Unit =
- _rc.synchronized { _rc = Process_Result.RC.merge(_rc, rc) }
+ _rc.change(rc0 => Process_Result.RC.merge(rc0, rc))
def capture[A](host: Build_Cluster.Host, op: String)(
e: => A,