tuned;
authorwenzelm
Sun May 07 13:20:24 2017 +0200 (2017-05-07)
changeset 65751426d4bf3b9bb
parent 65750 7f5556f4b584
child 65752 ed7b5cd3a7f2
tuned;
src/Pure/Admin/build_status.scala
     1.1 --- a/src/Pure/Admin/build_status.scala	Sat May 06 21:28:41 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sun May 07 13:20:24 2017 +0200
     1.3 @@ -62,7 +62,7 @@
     1.4      val store = Build_Log.store(options)
     1.5      using(store.open_database())(db =>
     1.6      {
     1.7 -      for (profile <- profiles) {
     1.8 +      for (profile <- profiles.sortBy(_.name)) {
     1.9          progress.echo("input " + quote(profile.name))
    1.10          val columns =
    1.11            List(