proper operation in weakly-typed Scala (amending 06153e2e0cdb);
authorwenzelm
Fri, 25 Jan 2019 15:57:24 +0100
changeset 69740 18d383f41477
parent 69739 8b47c021666e
child 69741 ac9704fd0935
proper operation in weakly-typed Scala (amending 06153e2e0cdb);
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)))
             }
           }