clarified worker state: always maintain database content via worker_uuid;
clarified message;
--- a/src/Pure/Tools/build_process.scala Wed Mar 08 13:33:18 2023 +0100
+++ b/src/Pure/Tools/build_process.scala Wed Mar 08 13:36:40 2023 +0100
@@ -144,7 +144,7 @@
build_heap || Sessions.is_pure(name) ||
sessions.valuesIterator.exists(_.ancestors.contains(name))
- def worker: Boolean = max_jobs > 1
+ def worker_active: Boolean = max_jobs > 1
}
@@ -921,8 +921,10 @@
else {
if (build_context.master) start_build()
- val worker = build_context.worker
- if (worker) start_worker() else progress.echo("Waiting for external workers ...")
+ start_worker()
+ if (build_context.master && !build_context.worker_active) {
+ progress.echo("Waiting for external workers ...")
+ }
try {
while (!finished()) {
@@ -946,7 +948,7 @@
}
}
finally {
- if (worker) stop_worker()
+ stop_worker()
if (build_context.master) stop_build()
}