# HG changeset patch
# User wenzelm
# Date 1688305191 -7200
# Node ID 39e1562e69cdc4b6889567108a8fdd089973e214
# Parent  1ddbeb791f30e56725115b7eddcd113f36575842
tuned;

diff -r 1ddbeb791f30 -r 39e1562e69cd src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Sun Jul 02 15:25:12 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Sun Jul 02 15:39:51 2023 +0200
@@ -551,10 +551,11 @@
       stop: Boolean = false
     ): Unit = {
       val sql =
+
+      db.execute_statement(
         Workers.table.update(List(Workers.stamp, Workers.stop, Workers.serial),
-          sql = Workers.worker_uuid.where_equal(worker_uuid))
-      db.execute_statement(sql, body =
-        { stmt =>
+          sql = Workers.worker_uuid.where_equal(worker_uuid)),
+        body = { stmt =>
           val now = db.now()
           stmt.date(1) = now
           stmt.date(2) = if (stop) Some(now) else None
@@ -1075,8 +1076,8 @@
     }
     else {
       if (build_context.master) start_build()
+      start_worker()
 
-      start_worker()
       if (build_context.master && !build_context.worker_active) {
         progress.echo("Waiting for external workers ...")
       }