On Mon, Apr 13, 2020 at 07:55:07PM -0400, Robert Haas wrote:
> Oh, hmm. Maybe I'm getting confused with a previous version of the
> patch that behaved differently.
No problem. If you prefer keeping this part of the code, that's fine
by me. If you think that the patch is suited as-is, including
silencing the error forcing to use --no-manifest on server versions
older than v13, I am fine to help out and apply it myself, but I am
also fine if you wish to take care of it by yourself.
--
Michael