From: Daniel Arndt Date: Fri, 25 Oct 2024 13:38:39 +0000 (-0400) Subject: Merge pull request #17803 from bangerth/strings-2 X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=7abb9c36645380a51c732797c5b616015e9467bf;p=dealii.git Merge pull request #17803 from bangerth/strings-2 --- 7abb9c36645380a51c732797c5b616015e9467bf