src/Pure/Admin/build_history.scala
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)
     }
   }