> On 20 May 2020, at 11:52, Peter Eisentraut <peter.eisentraut@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