# HG changeset patch
# User wenzelm
# Date 1494156024 -7200
# Node ID 426d4bf3b9bb9198f8ccbd39de52f1a36668a2d4
# Parent  7f5556f4b5846f0f49d620fe981584f8a592220d
tuned;

diff -r 7f5556f4b584 -r 426d4bf3b9bb src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sat May 06 21:28:41 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Sun May 07 13:20:24 2017 +0200
@@ -62,7 +62,7 @@
     val store = Build_Log.store(options)
     using(store.open_database())(db =>
     {
-      for (profile <- profiles) {
+      for (profile <- profiles.sortBy(_.name)) {
         progress.echo("input " + quote(profile.name))
         val columns =
           List(