diff -r c3a3db450c80 -r 1384593459b4 src/Pure/Tools/build_cluster.scala --- 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,