Re: [PATCH] ci: github action - add check for whitespace errors

From: Jeff King <peff@peff.net>
Date: Sep 22, 2020, 17:07 UTC
Message-ID: <20200922170745.GA541915@coredump.intra.peff.net>
In-Reply-To: <pull.709.git.1600759684548.gitgitgadget@gmail.com>

On Tue, Sep 22, 2020 at 07:28:04AM +0000, Chris. Webster via GitGitGadget wrote:

Show 5 quoted lines

> From: "Chris. Webster" <chris@webstech.net>
> 
> Not all developers are aware of `git diff --check` to warn
> about whitespace issues.  Running a check when a pull request is
> opened or updated can save time for reviewers and the submitter.

Sounds like a useful thing to have.

> A GitHub workflow will run when a pull request is created or the
> contents are updated to check the patch series.  A pull request
> provides the necessary information (number of commits) to only
> check the patch series.

I think this will work OK in practice, but a few thoughts:

 - for a linear branch on top of master, using the commit count will
   work reliably. But I suspect it would run into problems if there were
   ever a merge on a PR (e.g., back-merging from master), where we'd be
   subject to how `git log` linearizes the commits. That's not really a
   workflow I'd expect people to use with git.git, but it would probably
   be easy to make it more robust. Does the PR object provide the "base"
   oid, so we could do "git log $base..$head"?

 - this will run only on PRs. That's helpful for people using
   GitGitGadget, but it might also be useful for people just running the
   CI by pushing branches, or looking at CI builds of Junio's next or
   seen branches. Could we make it work there? Obviously we wouldn't be
   able to rely on having PR data, but I wonder if "git log
   HEAD..$branch" would be sufficient.

-Peff