On Thu, May 16, 2024 at 8:42 PM Robert Haas <robertmhaas(at)gmail(dot)com> wrote:
> You don't need to wait for the next CommitFest to fix a comment (or a
> bug). And, indeed, it's better if you do this before we branch.
Patch pushed and the CF entry closed. Thank you for the suggestion.
Thanks
Richard