On Thu, Feb 23, 2023 at 5:03 AM Andrew Dunstan <andrew@dunslane.net> wrote: > > I suspect not allowing // is at least a minor annoyance to any new developer we acquire under the age of about 40.
pgindent changes those to our style, so it's not much of an annoyance if one prefers to type it that way during development.