src/Pure/Tools/build.scala

--- a/src/Pure/Tools/build.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Tools/build.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -159,8 +159,8 @@
     def apply(name: String): Process_Result = results(name)._1.getOrElse(Process_Result(1))
     def info(name: String): Sessions.Info = results(name)._2
     val rc: Int =
-      (0 /: results.iterator.map(
-        { case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }))(_ max _)
+      results.iterator.map({ case (_, (Some(r), _)) => r.rc case (_, (None, _)) => 1 }).
+        foldLeft(0)(_ max _)
     def ok: Boolean = rc == 0
 
     override def toString: String = rc.toString
@@ -661,7 +661,7 @@
     }
 
     val total_timing =
-      (Timing.zero /: results.sessions.iterator.map(a => results(a).timing))(_ + _).
+      results.sessions.iterator.map(a => results(a).timing).foldLeft(Timing.zero)(_ + _).
         copy(elapsed = elapsed_time)
     progress.echo(total_timing.message_resources)