# HG changeset patch
# User wenzelm
# Date 1690110555 -7200
# Node ID 001d423daf7c0fd121b4b3940584b911adcbc849
# Parent  d79eb2a6de0f19439dce48611ba7aaf9b09ba58b
prefer Process_Result.RC.merge: strict treatment of interrupt;

diff -r d79eb2a6de0f -r 001d423daf7c src/HOL/Tools/Nitpick/kodkod.scala
--- a/src/HOL/Tools/Nitpick/kodkod.scala	Sun Jul 23 12:59:52 2023 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.scala	Sun Jul 23 13:09:15 2023 +0200
@@ -62,7 +62,7 @@
       private val out = new StringBuilder
       private val err = new StringBuilder
 
-      def return_code(i: Int): Unit = synchronized { rc = rc max i}
+      def return_code(i: Int): Unit = synchronized { rc = Process_Result.RC.merge(rc, i) }
 
       override def output(s: String): Unit = synchronized {
         Exn.Interrupt.expose()
diff -r d79eb2a6de0f -r 001d423daf7c src/Pure/Admin/build_history.scala
--- a/src/Pure/Admin/build_history.scala	Sun Jul 23 12:59:52 2023 +0200
+++ b/src/Pure/Admin/build_history.scala	Sun Jul 23 13:09:15 2023 +0200
@@ -519,7 +519,7 @@
           cat_lines(for ((_, log_path) <- results) yield log_path.implode))
       }
 
-      val rc = results.foldLeft(Process_Result.RC.ok) { case (rc, (res, _)) => rc max res.rc }
+      val rc = Process_Result.RC.merge(results.map(p => p._1.rc))
       if (rc != Process_Result.RC.ok && exit_code) sys.exit(rc)
     }
   }