# HG changeset patch
# User wenzelm
# Date 1709583504 -3600
# Node ID 7e05515cadc07873b0ec615bd46f16476cbbc35b
# Parent  52b5c7c8e6d9df5d0d9cef043c826f98e38829f7
omit somewhat pointless message, following b7187d4cdf68;

diff -r 52b5c7c8e6d9 -r 7e05515cadc0 src/Pure/Build/build_process.scala
--- a/src/Pure/Build/build_process.scala	Mon Mar 04 20:49:46 2024 +0100
+++ b/src/Pure/Build/build_process.scala	Mon Mar 04 21:18:24 2024 +0100
@@ -1171,10 +1171,6 @@
       start_worker()
       _build_cluster.start()
 
-      if (build_context.master && !build_context.worker && _build_cluster.active()) {
-        build_progress.echo("Waiting for external workers ...")
-      }
-
       try {
         while (!finished) {
           val check_jobs =