Making makeinfo html-happy

Fixes for warnings issued by makeinfo 5.x (when using some of our
macros: the guy is touchy regarding @ifhtml and new lines) that were
preventing the install-html make target to work (for people that want
local html by texinfo as opposed to the (supposedly fancier)
texi2html-generated version we use for the web).