Re: [help-texinfo] html output (footnotes)

[Patrice Dumas]

On Sat, Mar 02, 2019 at 08:46:01PM +0000, Gavin Smith wrote:
> 
> I agree that the second would make more sense.
> 
> Does anybody know or want to check if there was any reason for this?

I did the code, but I do not think I did the choice of headers like that
on purpose.  A possibility, but I haven't checked, is that the strange
result could come from mixing texi2html and makeinfo styles.

In any case I am not opposed to changing that, I agree that it would be
more consistent to have the footnote numbers smaller at least same size
as the header.  For the "footnote header" part, it is possible that the
size is setup such that it is not too big compared to the section
header, so maybe it would be better not to change this header size.

-- 
Pat