> On 6 Nov 2024, at 15:51, Alvaro Herrera <alvhe...@alvh.no-ip.org> wrote: > > On 2024-Nov-06, Daniel Gustafsson wrote: > >> Committed, and with some help from Magnus, the docs site has been reloaded >> with >> the new CSS. Everything seems to behave as expected when testing in Firefox, >> Safari, Chrome and Edge. > > Ah, but we kept the #? I thought it was going to be changed to ¶ ... > was there any voice against that?
You're right, I mistakenly remembered there being no concensus and didn't re-read the thread when it was revived with the patch in question. Re-reading it now I see multiple +1's for using a ¶ instead so will fix that. Thanks for the heads-up. -- Daniel Gustafsson
