Merge branch '16-repo-documentation' into 'dev'
Resolve "Repo documentation" See merge request !1
GitLab update scheduled for Friday, July 8th between 08:15 and 08:45 CET. If unpleasant, please contact René or Martin.
Resolve "Repo documentation" See merge request !1