# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1720533992 -7200
# Node ID 1dd989a9ad886dd50199876e43ea288e30f8a193
# Parent  06c80577f5891352d1f2cf0ffce48b3d98d62d7b
tuned display;

diff -r 06c80577f589 -r 1dd989a9ad88 src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Tue Jul 09 16:00:25 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Tue Jul 09 16:06:32 2024 +0200
@@ -1280,10 +1280,11 @@
         def render_diff(data: Report.Data, components: List[Component]): XML.Body =
           par(List(page_link(Page.BUILD, "back to build", Markup.Name(build.name)))) ::
           (for (component <- components if !component.is_local) yield {
-            par(
-              text(component.name) :::
+            val infos = 
               data.component_logs.toMap.get(component.name).toList.flatMap(colored) :::
-              data.component_diffs.toMap.get(component.name).toList.flatMap(colored))
+              data.component_diffs.toMap.get(component.name).toList.flatMap(colored)
+
+            par(if (infos.isEmpty) text(component.toString) else text(component.name) ::: infos)
           })
 
         build match {