From: Matthias Maier Date: Sat, 17 Aug 2024 06:05:43 +0000 (+0000) Subject: Merge pull request #17559 from marcfehling/doc-worker X-Git-Url: https://gitweb.dealii.org/cgi-bin/gitweb.cgi?a=commitdiff_plain;h=c06e4c2d9fcb11edac120724fd5bcd2977dfb315;p=dealii.git Merge pull request #17559 from marcfehling/doc-worker Outsource building documentation into separate github workflow. --- c06e4c2d9fcb11edac120724fd5bcd2977dfb315