GitLab

This makes no difference to anything, since we always use makeinfo -o,
but it makes automake happier, if we ever decide to use that.