diff -r 69d3547206db -r 32f9e75c92e9 src/Pure/Tools/build_process.scala --- 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() }