# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1710944360 -3600
# Node ID 7a7f1d5dcfe94273788647844b1d2920da87a7ae
# Parent  502525a82d9f12aa934ca2cc0a0b73b689c565b7
only print schedule if relevant;

diff -r 502525a82d9f -r 7a7f1d5dcfe9 src/Pure/Build/build_schedule.scala
--- a/src/Pure/Build/build_schedule.scala	Wed Mar 20 16:23:26 2024 +0100
+++ b/src/Pure/Build/build_schedule.scala	Wed Mar 20 15:19:20 2024 +0100
@@ -1150,7 +1150,9 @@
           val elapsed = Time.now() - start
 
           val timing_msg = if (elapsed.is_relevant) " (took " + elapsed.message + ")" else ""
-          progress.echo_if(_schedule.deviation(schedule).minutes > 1, schedule.message + timing_msg)
+          progress.echo_if(
+            _schedule.deviation(schedule).minutes > 1 && schedule.duration >= Time.seconds(1),
+            schedule.message + timing_msg)
 
           _schedule = schedule
           _schedule.next(hostname, state)