src/Pure/Admin/build_history.scala
changeset 73359 d8a0e996614b
parent 73340 0ffcad1f6130
child 73522 b219774a71ae
--- a/src/Pure/Admin/build_history.scala	Wed Mar 03 22:48:46 2021 +0100
+++ b/src/Pure/Admin/build_history.scala	Thu Mar 04 15:41:46 2021 +0100
@@ -519,7 +519,7 @@
           cat_lines(for ((_, log_path) <- results) yield log_path.implode))
       }
 
-      val rc = (0 /: results) { case (rc, (res, _)) => rc max res.rc }
+      val rc = results.foldLeft(0) { case (rc, (res, _)) => rc max res.rc }
       if (rc != 0 && exit_code) sys.exit(rc)
     }
   }