From: Daniel Arndt Date: Fri, 13 Jan 2023 18:17:02 +0000 (-0500) Subject: Merge pull request #14676 from luca-heltai/stefanozampini/minor X-Git-Tag: v9.5.0-rc1~653 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=3ff256e8e351f0a6586affd9bc48c25b6987ce65;p=dealii.git Merge pull request #14676 from luca-heltai/stefanozampini/minor --- 3ff256e8e351f0a6586affd9bc48c25b6987ce65