This contains a set of small, mostly cosmetic, changes.
In a few places I have put FIXMEs, so this should not be directly merged, but rather adjusted before, depending on what the answer to the FIXME is.
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.
This contains a set of small, mostly cosmetic, changes.
In a few places I have put FIXMEs, so this should not be directly merged, but rather adjusted before, depending on what the answer to the FIXME is.