# HG changeset patch
# User wenzelm
# Date 1688557305 -7200
# Node ID 4dca4ba6f01b1c805c8d476d9113f103af5a5eba
# Parent  f0762eb07583d72f1fc49d6ee0aca788ec65ae5d
proper build_progress for local messages;

diff -r f0762eb07583 -r 4dca4ba6f01b src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Jul 05 11:27:36 2023 +0200
+++ b/src/Pure/Tools/build_process.scala	Wed Jul 05 13:41:45 2023 +0200
@@ -1081,7 +1081,7 @@
       start_worker()
 
       if (build_context.master && !build_context.worker_active) {
-        progress.echo("Waiting for external workers ...")
+        build_progress.echo("Waiting for external workers ...")
       }
 
       try {