GitLab

[This reapplies part of commit
3ffe81e2,
which was inadvertently lost by merge commit
7823745a.]
(Bug#22202)