changeset 74306 | a117c076aa22 |
parent 74036 | 57768f30d17c |
child 75393 | 87ebf5a50283 |
--- a/src/Pure/Admin/build_history.scala Sun Sep 12 22:31:51 2021 +0200 +++ b/src/Pure/Admin/build_history.scala Mon Sep 13 11:52:32 2021 +0200 @@ -525,8 +525,8 @@ cat_lines(for ((_, log_path) <- results) yield log_path.implode)) } - val rc = results.foldLeft(0) { case (rc, (res, _)) => rc max res.rc } - if (rc != 0 && exit_code) sys.exit(rc) + val rc = results.foldLeft(Process_Result.RC.ok) { case (rc, (res, _)) => rc max res.rc } + if (rc != Process_Result.RC.ok && exit_code) sys.exit(rc) } }