From: David Wells Date: Fri, 23 May 2025 12:22:19 +0000 (-0400) Subject: Merge pull request #18484 from bangerth/detour X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=c64348ffbabb80f733d31b2e0563e166934ae144;p=dealii.git Merge pull request #18484 from bangerth/detour Avoid an unnecessary detour. --- c64348ffbabb80f733d31b2e0563e166934ae144