On Thu, 2020-06-04 at 16:35 -0400, Alvaro Herrera wrote:
> If it is something worth worrying about, let's discuss what's a good
> fix for it.
I did post a fix for it, but it's not a very clean fix. I'm slightly
inclined to proceed with that fix, but I was hoping someone else would
have a better suggestion.
How about if I wait another week, and if we still don't have a better
fix, I will commit this one.
Regards,
Jeff Davis
