tuned website;
authorFabian Huch <huch@in.tum.de>
Fri, 28 Jun 2024 12:10:26 +0200
changeset 80421 96e1b4f38a17
parent 80420 80e10a1aa431
child 80422 23569f8a62e9
tuned website;
src/Pure/Build/build_manager.scala
--- a/src/Pure/Build/build_manager.scala	Fri Jun 28 11:51:46 2024 +0200
+++ b/src/Pure/Build/build_manager.scala	Fri Jun 28 12:10:26 2024 +0200
@@ -1074,7 +1074,7 @@
 
         text("Queue: " + state.pending.size + " tasks waiting") :::
         section("Builds") :: par(text("Total: " + state.num_builds + " builds")) ::
-        state.kinds.map(render_kind)
+        state.kinds.sorted.map(render_kind)
       }
 
       def render_overview(kind: String, state: State): XML.Body =