On Sun, Feb 18, 2018 at 8:23 AM, Marko Tiikkaja <marko(at)joh(dot)to> wrote:
> Does anyone care to care about this? We've had two report of what I think
> is the same problem, yet nobody's properly analyzed the problem.
I didn't notice this until now. I'd say that it's certainly a bug, and
should be fixed.
--
Peter Geoghegan