Re: [O] make doc fails on current head

[Bastien]

Hi Jonathan,

Jonathan Leech-Pepin <jonathan.leechpe...@gmail.com> writes:

> Under the current git head (4144c55) I get the following error when
> trying to run =make doc=.

Fixed, thanks for reporting this.

-- 
 Bastien