On Mon, May 08, 2017 at 05:26:35PM +0200, Clément Lassieur wrote:
> * .gitignore: Add entry for the above directory which is created by 'make
> html'.

Thanks, LGTM