# HG changeset patch
# User wenzelm
# Date 1548428244 -3600
# Node ID 18d383f41477940818c3128ee99d1a10a53f804c
# Parent  8b47c021666e09cd9c3350939c72fd925597fac6
proper operation in weakly-typed Scala (amending 06153e2e0cdb);

diff -r 8b47c021666e -r 18d383f41477 src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Fri Jan 25 14:59:40 2019 +0100
+++ b/src/Pure/Admin/build_status.scala	Fri Jan 25 15:57:24 2019 +0100
@@ -320,7 +320,7 @@
               }
 
             if ((!afp || chapter == "AFP") &&
-                (!profile.bulky || groups.contains(AFP.groups_bulky.toSet))) {
+                (!profile.bulky || groups.exists(AFP.groups_bulky.toSet))) {
               data_entries += (data_name -> (sessions + (session_name -> session)))
             }
           }