Commit 9c0cb981 authored Jun 23, 2025 by Arjo Segers

Merge branch 'pages' into 'master'

Fixed generation of documentation on GitLab pages.

See merge request !13