Michael Paquier <michael.paquier@gmail.com> writes:
> Actually I am sending an updated patch as buildenv.pl enters in the
> same category as config.pl.
This seems sane to me; it's in the same category as src/Makefile.custom,
which we have a .gitignore entry for. I wondered whether there were any
more such files, but the documentation at least doesn't mention any.
regards, tom lane