On Tue, Jul 2, 2024 at 6:22 PM Richard Guo <guofenglinux@gmail.com> wrote:
> Here is an updated patch, with some tweaks suggested by pgindent, and
> adjustments to the commit message suggested by Andrew (off-list).
>
> Barring objections, I'm planning to push it next week.
Pushed. Thank you for the report. The fix will appear in August's
minor releases.
Thanks
Richard