GitLab

This reverts commit 2f5e0b1b.
I see no reason for removing code, documentation, and comments
in the original commit.