Re: [PATCH v2 3/5] gitlab: build HTML documentation