--- 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 ...")
}