From: Marc Fehling Date: Sun, 19 Jan 2025 12:39:42 +0000 (+0100) Subject: Merge pull request #18010 from drwells/deprecated-headers X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=6e04ac39aa3d469dceda5cc6466ad342e6e20c53;p=dealii.git Merge pull request #18010 from drwells/deprecated-headers Consistently format deprecated headers. --- 6e04ac39aa3d469dceda5cc6466ad342e6e20c53