From: Jeff King <peff@peff.net>
Date: Sat, 23 Sep 2023 07:00:19 GMT
Subject: Re: [PATCH 3/6] coverity: allow overriding the Coverity project
Message-ID: <20230923070019.GD1469941@coredump.intra.peff.net>
In-Reply-To: <6c1c82862814f40a408231cb249fb4b653276b52.1695379323.git.gitgitgadget@gmail.com>

On Fri, Sep 22, 2023 at 10:42:00AM +0000, Johannes Schindelin via GitGitGadget wrote:

> +# By default, the builds are submitted to the Coverity project `git`. To override this,
> +# set the repository variable `COVERITY_PROJECT`.

This may not matter all that much, because I don't expect most people to
set this up for their forks (and if we have git/git results that I have
access to, I will probably even stop building my peff/git one). But I
just wondered if a better default would be the GitHub project name
(i.e., $user/git).

It has been long enough that I do not remember all of the setup on the
Coverity side, but I assumed there was some "set it up for this GitHub
project" button. But maybe I just picked that name myself.

-Peff