> On 20 May 2020, at 11:52, Peter Eisentraut <peter.eisentr...@2ndquadrant.com> > wrote:
> Or should this file be excluded, since it's generated? That would get my vote. Generated files where we don't control the generator can be excluded. cheers ./daniel
