Merge branch 'cherry-pick-1d837397' into 'releases/2.8' (!393) · Merge requests · staging / dune-functions · GitLab

Oliver Sander requested to merge cherry-pick-6a20d8a8 into releases/2.8 Jan 04, 2023

Merge branch 'issue/install-missing-headers' into 'master'

See merge request !392 (merged)

(cherry picked from commit 6a20d8a8)

5549cb30 Merge branch 'issue/install-missing-headers' into 'master'