src/Pure/Admin/build_status.scala
changeset 69693 06153e2e0cdb
parent 69277 258bef08b31e
child 69734 e58f158c8ac5
--- a/src/Pure/Admin/build_status.scala	Sat Jan 19 19:16:58 2019 +0100
+++ b/src/Pure/Admin/build_status.scala	Sat Jan 19 20:18:26 2019 +0100
@@ -22,7 +22,7 @@
   /* data profiles */
 
   sealed case class Profile(
-    description: String, history: Int = 0, afp: Boolean = false, slow: Boolean = false, sql: String)
+    description: String, history: Int = 0, afp: Boolean = false, bulky: Boolean = false, sql: String)
   {
     def days(options: Options): Int = options.int("build_log_history") max history
 
@@ -319,7 +319,8 @@
                   Session(session_name, threads, entry :: old.entries, ml_stats1, ml_stats1_date)
               }
 
-            if ((!afp || chapter == "AFP") && (!profile.slow || groups.contains("slow"))) {
+            if ((!afp || chapter == "AFP") &&
+                (!profile.bulky || groups.contains(AFP.groups_bulky.toSet))) {
               data_entries += (data_name -> (sessions + (session_name -> session)))
             }
           }