Making makeinfo html-happy
commit586d552350c04f4025ce99d2600bf89496db6e31
authorJose Antonio Ortega Ruiz <jao@gnu.org>
Sat, 31 May 2014 03:37:09 +0000 (31 05:37 +0200)
committerJose Antonio Ortega Ruiz <jao@gnu.org>
Sat, 31 May 2014 03:37:09 +0000 (31 05:37 +0200)
tree3fd56827bf2004dc84204a52e7454805aaa16a35
parent5020b91e90520a9e5c0c725123247535dfb60a4f
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).
doc/parens.texi
doc/repl.texi