On Thu, 7 Nov 2024 at 03:58, Daniel Gustafsson <[email protected]> wrote: > > > On 6 Nov 2024, at 15:51, Alvaro Herrera <[email protected]> wrote: > > 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.
I see in the release notes we're using §. I'm not advocating for any particular one, but would it make sense to be consistent on which character we use for this? David
