I almost missed Christian's last commit. It was poor luck 🍀 that I had a look into the commit history before replacing the old remote URL by the new, Gitlab-based one. I manually transferred his commit and saved myself the work of programming what Christian already did.