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
