# HG changeset patch
# User wenzelm
# Date 1692781230 -7200
# Node ID a97d2b6b5c3e93f7f0e80b0b14dc4649b0a285fb
# Parent  db99a70f8531728e1aadc8cdc4c1e97bf4798556
tuned signature;

diff -r db99a70f8531 -r a97d2b6b5c3e src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Aug 22 13:51:06 2023 +0200
+++ b/src/Pure/Tools/build.scala	Wed Aug 23 11:00:30 2023 +0200
@@ -580,7 +580,7 @@
     dirs: List[Path] = Nil,
     numa_shuffling: Boolean = false,
     max_jobs: Int = 1
-  ): Option[Results] = {
+  ): Results = {
     val build_engine = Engine(engine_name(options))
     val store = build_engine.build_store(options)
     val build_options = store.options
@@ -603,7 +603,7 @@
             hostname = hostname(build_options), numa_shuffling = numa_shuffling,
             max_jobs = max_jobs, build_uuid = build_master.build_uuid)
 
-        Some(build_engine.run_build_process(build_context, progress, server))
+        build_engine.run_build_process(build_context, progress, server)
       }
     }
   }
@@ -646,7 +646,7 @@
 
       val progress = new Console_Progress(verbose = verbose)
 
-      val res =
+      val results =
         progress.interrupt_handler {
           build_worker(options,
             build_id = build_id,
@@ -657,10 +657,7 @@
             max_jobs = max_jobs)
         }
 
-      res match {
-        case Some(results) if !results.ok => sys.exit(results.rc)
-        case _ =>
-      }
+      if (!results.ok) sys.exit(results.rc)
     })