--- 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 {