Peter Eisentraut <peter@eisentraut.org> writes:
> On 23.01.24 15:08, Tom Lane wrote:
>> Per guaibasaurus[1], this commit broke "make dist":
>> I'm not sure why --- the makefile changes treat these new files
>> exactly like other generated files. It doesn't repro here,
>> either, which is odd. It looks like a timing problem, but how
>> could there be one?
> I have found that the files are not listed in the clean target in
> src/include/Makefile. That might explain it, but it's gotta be fixed
> anyway. I'll go ahead with that.
Looks like that made guaibasaurus happy, but I'm still mystified
as to what was wrong and why it didn't repro elsewhere.
regards, tom lane