# HG changeset patch
# User wenzelm
# Date 1693050423 -7200
# Node ID 1384593459b49085159eb29284d388da189f5419
# Parent  c3a3db450c80d7ff4cdcf0120d3b80c6c3b4172a
tuned: prefer explicit types;

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,