From: Matthias Maier <tamiko@43-1.org>
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