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 "#": https://www.postgresql.org/docs/devel/tutorial-arch.html I am actually fine with "#" since that is the symbol that will be added to the URL. -- Bruce Momjian <br...@momjian.us> https://momjian.us EDB https://enterprisedb.com When a patient asks the doctor, "Am I going to die?", he means "Am I going to die soon?"