> On 18 Nov 2024, at 20:51, Bruce Momjian <br...@momjian.us> wrote: > > On Wed, Nov 6, 2024 at 03:58:18PM +0100, Daniel Gustafsson wrote: >>> 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. > > Uh, has this change been made? I still see "#":
It hasn't been changed, I was hoping to hear more opinions but since there has been none I will go ahead with the result of the previous discussion which landed in ¶. Hearing no complaints against the fix for the issue Álvaro identified I'll push that as well. -- Daniel Gustafsson
