Hi Ludo,

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

Thank you,

John