author | wenzelm |
Sun, 07 May 2017 13:20:24 +0200 | |
changeset 65751 | 426d4bf3b9bb |
parent 65750 | 7f5556f4b584 |
child 65752 | ed7b5cd3a7f2 |
--- 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(