On Thu, May 16, 2024 at 8:42 PM Robert Haas <robertmh...@gmail.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
