Nathan Bossart <nathandbossart@gmail.com> writes:
> On Tue, May 14, 2024 at 10:05:01AM +0200, Peter Eisentraut wrote:
>> My point is, in order to get that enhanced GitHub experience, you don't
>> actually have to commit these files into the individual source code
>> repository. You can add them to the organization and they will apply to all
>> repositories under the organization. This is explained at the above link.
> Oh, I apologize, my brain skipped over the word "organization" in your
> message.
FWIW, I'd vote against doing it that way, because then
maintaining/updating those files would only be possible for whoever
owns the github repo. I don't have a position on whether we want
these additional files or not; but if we do, I think the best answer
is to stick 'em under .github/ where they are out of the way but yet
updatable by any committer.
regards, tom lane
