> This is very strange; I didn't get that error.  We've got makeinfo 6.1
> (Feb 2016) installed here.  Are you using a newer or older version?

It's makeinfo 4.13 (from the vendor).

-- 
Eric Botcazou

Reply via email to