From: Bruno Blais Date: Sat, 1 Mar 2025 20:34:49 +0000 (-0500) Subject: Merge pull request #18183 from bangerth/warning X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=bc157d47c240ce8db0d677a33f7bf034d391c57a;p=dealii.git Merge pull request #18183 from bangerth/warning Avoid a warning about an unused variable. --- bc157d47c240ce8db0d677a33f7bf034d391c57a