# HG changeset patch
# User wenzelm
# Date 1509557079 -3600
# Node ID e76c6cb0d4612ff70879d58bb7fc46e2b587a0ac
# Parent  8947cf58cb866df95a28af7b6ed5f69e2a10737d
proper order for entries from multiple profiles, notably "AFP";

diff -r 8947cf58cb86 -r e76c6cb0d461 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Wed Nov 01 17:29:14 2017 +0100
+++ b/src/Pure/Admin/build_status.scala	Wed Nov 01 18:24:39 2017 +0100
@@ -41,8 +41,7 @@
               Build_Log.Session_Status.failed.toString)) +
           (if (only_sessions.isEmpty) ""
            else " AND " + SQL.member(Build_Log.Data.session_name.ident, only_sessions)) +
-          " AND " + SQL.enclose(sql) +
-          " ORDER BY " + Build_Log.Data.pull_date(afp))
+          " AND " + SQL.enclose(sql))
     }
   }
 
@@ -80,6 +79,9 @@
   {
     require(entries.nonEmpty)
 
+    def sort_entries: Session =
+      copy(entries = entries.sortBy(entry => - entry.pull_date.unix_epoch))
+
     def head: Entry = entries.head
     def order: Long = - head.timing.elapsed.ms
 
@@ -261,7 +263,7 @@
     val sorted_entries =
       (for {
         (name, sessions) <- data_entries.toList
-        sorted_sessions <- proper_list(sessions.toList.map(_._2).sortBy(_.order))
+        sorted_sessions <- proper_list(sessions.toList.map(p => p._2.sort_entries).sortBy(_.order))
       }
       yield {
         val hosts = get_hosts(name).toList.sorted