GitLab

Since !35 (closed) is still not merged (and it's already missing more fixes we want) let's c'n'p two important ones for the devkit release.