tuned display;
authorFabian Huch <huch@in.tum.de>
Tue, 09 Jul 2024 16:06:32 +0200
changeset 80538 1dd989a9ad88
parent 80537 06c80577f589
child 80539 34a5ca6fcddd
tuned display;
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 {