From: Matthias Maier Date: Tue, 25 Mar 2025 05:32:32 +0000 (+0000) Subject: Merge pull request #18219 from bangerth/detailed X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=4274414461ca7cb8a0f02b50784ff7025ef870a1;p=dealii.git Merge pull request #18219 from bangerth/detailed Minor cleanup in reporting in detailed.log. --- 4274414461ca7cb8a0f02b50784ff7025ef870a1