On Fri, Jul 25, 2025 at 05:41:30PM +0100, Gavin Smith wrote: > I don't agree with specifying "font-size: 150%" for the index letter > headers, as we shouldn't be specifying exact ratios of font sizes. As > I said, the previous formatting looked fine, so we could try to imitate > this, even if we eliminate the first empty table column used for indenting > the menu (which I believe was the main aspect of the previous formatting > that people were objecting to). But if we did want a larger header, > we could use some heading command like <h2>, or possibly using a CSS > keyword like "font-size: larger". > > I am shortly going to commit a change to remove "font-size: 150%", while > working out the details of vertical and horizontal spacing will possibly > take me a lot longer.
I've made a few changes and am quite happy with the HTML index formatting now. I've used "font-size: larger" for the letter headers. I have not tried to indent the index entries under the headers as I didn't think it was really necessary.
