--- a/src/Pure/Build/build_manager.scala Wed Jul 10 17:31:17 2024 +0200
+++ b/src/Pure/Build/build_manager.scala Wed Jul 10 17:42:48 2024 +0200
@@ -1229,8 +1229,8 @@
val hg_info = data.component_logs.map(_._1) ++ data.component_diffs.map(_._1)
val s = components.mkString(", ")
- if (!components.map(_.name).exists(hg_info.toSet)) text(s)
- else List(page_link(Page.DIFF, s, Markup.Name(build.name)))
+ if (!components.map(_.name).exists(hg_info.toSet)) text("Components: " + s)
+ else text("Components: ") :+ page_link(Page.DIFF, s, Markup.Name(build.name))
}
build match {
@@ -1287,7 +1287,8 @@
data.component_logs.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)
+ val header = if (infos.isEmpty) component.toString else component.name + ":"
+ par(subsubsection(header) :: infos)
})
build match {