Hi Ludo,

I am not familiar with the info and html documentation build process. Will this patch suffice?

Thank you,

John