Michael Paquier <michael(dot)paquier(at)gmail(dot)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