Re: [PATCH 3/6] coverity: allow overriding the Coverity project
- From
Junio C Hamano <gitster@pobox.com>
- Date
- Sep 26, 2023, 16:50 UTC
- Message-ID
- <xmqqh6ngop43.fsf@gitster.g>
- In-Reply-To
- <20230926143933.GA1897653@coredump.intra.peff.net>
Jeff King <peff@peff.net> writes:
Show 25 quoted lines
> On Tue, Sep 26, 2023 at 07:19:46AM -0700, Junio C Hamano wrote: > >> At the same time, it would be one less thing they need to tweak >> before starting to use it, and if there are two or more users to do >> so, it would already have paid off. Developers typically outnumber >> projects they work on. >> >> I also have to wonder if it might make it more obvious what is going >> on if you made the default to $user/$fork and have the project >> override it, which hopefully may make it easier to find out what >> they need to do for those who want to override it to a different >> value to suit their need? > > Yeah, that was my thinking (and what I had been proposing). > > But I really think it probably doesn't matter that much either way. I > would not be surprised if there are zero developers who use this, > because of the setup on the coverity side, and the fact that the results > are not always immediately actionable. > > Even I, who has been running coverity on my local fork for a few years, > will probably just switch to using the git.git run and occasionally > looking at the results (that creates an extra headache because somebody > has to grant acess to the git.git run results to interested parties, but > it's also a one-time setup thing).
Sure.
I do not care too much either way, and in a situation like this where the design decision does not have a crucial longer-term impact either way exactly because it is a one-time thing for any user, whoever has invested their work on should have the final say.
Thanks.