On Wed, 2023-05-17 at 13:39 -0400, Kirk Wolak wrote:
> Here's the patch.
You removed the ******** QUERY ******** at the end of the query.
I think we should keep that (as comments, of course). People
are used to the current output, and it is nice to have a clear
visual marker at the end of what isn't normally part of "psql"
output.
"okbob" should be "Pavel Stehule".
Yours,
Laurenz Albe