I propose to merge this with the main branch after a small revision (thus WIP prefix for now).
On Monday, June 12, 2023, from 9.00 to 10.00 am there will be a maintenance with a short downtime of the GitLab service.
I propose to merge this with the main branch after a small revision (thus WIP prefix for now).