On Sat, Oct 7, 2017 at 4:27 PM, Peter Geoghegan <pg(at)bowt(dot)ie> wrote:
> I suspect commit d8d32d9 is involved here, though I haven't verified that.
Weirdly, there is a git hash collision here, so you'll have to put in
d8d32d9a (8 characters -- the default of 7 for a short git hash isn't
cutting it).
--
Peter Geoghegan