# HG changeset patch
# User wenzelm
# Date 1692782407 -7200
# Node ID 50675688c4df0a494fafd9c6595bf9847de946ad
# Parent  a97d2b6b5c3e93f7f0e80b0b14dc4649b0a285fb
tuned;

diff -r a97d2b6b5c3e -r 50675688c4df src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Aug 23 11:00:30 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Wed Aug 23 11:20:07 2023 +0200
@@ -877,23 +877,21 @@
     catch { case exn: Throwable => close(); throw exn }
 
   protected val (progress, worker_uuid) = synchronized {
-    _build_database match {
-      case None => (build_progress, UUID.random().toString)
-      case Some(db) =>
-        try {
-          val progress_db =
-            store.open_build_database(Progress.private_data.database, server = server)
-          val progress =
-            new Database_Progress(progress_db, build_progress,
-              input_messages = build_context.master,
-              output_stopped = build_context.master,
-              hostname = hostname,
-              context_uuid = build_uuid,
-              kind = "build_process",
-              timeout = Some(build_delay))
-          (progress, progress.agent_uuid)
-        }
-        catch { case exn: Throwable => close(); throw exn }
+    if (_build_database.isEmpty) (build_progress, UUID.random().toString)
+    else {
+      try {
+        val db = store.open_build_database(Progress.private_data.database, server = server)
+        val progress =
+          new Database_Progress(db, build_progress,
+            input_messages = build_context.master,
+            output_stopped = build_context.master,
+            hostname = hostname,
+            context_uuid = build_uuid,
+            kind = "build_process",
+            timeout = Some(build_delay))
+        (progress, progress.agent_uuid)
+      }
+      catch { case exn: Throwable => close(); throw exn }
     }
   }