tuned website;
authorFabian Huch <huch@in.tum.de>
Wed, 10 Jul 2024 17:42:48 +0200
changeset 80547 819402eeac34
parent 80546 d507229c5771
child 80559 38c63d4027c4
tuned website;
src/Pure/Build/build_manager.scala
--- 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 {