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) } }