From: Peter Munch <peterrmuench@gmail.com>
Date: Tue, 19 Oct 2021 05:59:35 +0000 (+0200)
Subject: Merge pull request #12841 from bangerth/dif2
X-Git-Tag: v9.4.0-rc1~928
X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=84e3ecb0e0f4ec22d021cad93343008988fdc434;p=dealii.git

Merge pull request #12841 from bangerth/dif2

Simplify some code by using std::any_of().
---

84e3ecb0e0f4ec22d021cad93343008988fdc434