# 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))) } }