I wrote: > There's no obvious difference between bedda9fbb and 6dd690be3, > so I surmise that that patch depended somehow on some previous > work that only went into v11 not v10. Haven't found what, yet.
Ah, looks like it was 42e61c774. I'll push a fix shortly.
regards, tom lane
