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