# HG changeset patch # User Fabian Huch # Date 1719569426 -7200 # Node ID 96e1b4f38a173450090fde9d1c7665b5387ebc21 # Parent 80e10a1aa431984ea5020a3cbff6b0448923a772 tuned website; diff -r 80e10a1aa431 -r 96e1b4f38a17 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 =