On Thu, May 16, 2019 at 10:29:16PM -0400, Alvaro Herrera wrote:> Argh. Apologies, sorry for fixing so quickly.
No problem. The buildfarm does not complain anymore after the patch,so it looks that we are good.--Michael