[PATCH] Really execute the recipe of the 'docs' target in top-most Makefile

[Nicolas Sebrecht]

On Mon, Mar 21, 2016 at 12:59:38PM +0100, Dodji Seketeli wrote:

> Here is a git patch.

Thank you much Dodji!

Applied.

-- 
Nicolas Sebrecht