GitLab upgrade completed. Current version is 17.11.1. We now benefit from the features of the release 17.11.
Using ! to direct execute the compilation without needing to open a terminal
(This avoids breaking the workflow of the class)
Also adding some additional doc (it can be separated in a different MR, so doesn't mesh with the previous one)