tuned;
authorwenzelm
Sun, 02 Jul 2023 15:39:51 +0200
changeset 78241 39e1562e69cd
parent 78240 1ddbeb791f30
child 78242 633ae08625d1
tuned;
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 ...")
       }