commons-dev mailing list archives

Site index · List index
Message view « Date » · « Thread »
Top « Date » · « Thread »
From Matt Sicker <>
Subject Re: [ALL][Math] git pull requests: how?
Date Thu, 02 Mar 2017 04:51:54 GMT
Normally the GitHub email gives you the proper command to use to pull the
PR into your local git which you can merge and push (which merges the PR
once GitHub gets updated from

As for making sure that email gets sent, if it's not, file an INFRA ticket
about it. I've never tried it, but this might work:

git pull

If you add .diff or .patch to the end of the URL, it gives you a diff that
you can manually apply. The .diff URL appears to be a normal diff while the
.patch URL is the output of "git format-patch". So, if you download <> and run "git apply
55.patch", that'll commit it properly as if you merged the PR itself I
think (it'll set the commit author properly at least for proper historical

Also, adding a commit message somewhere (e.g., a follow up empty commit or
a changelog entry commit) containing the phrase "this closes #55" (or maybe
just "closes #55"; it's pretty loose) is enough to close the PR, but
merging it should close it automatically.

On 1 March 2017 at 17:53, Gilles <> wrote:

> Hi.
> How should the project be configured such that the request
> posted here:
> is as easy to handle as the one posted here:
> ?
> Thanks,
> Gilles
> ---------------------------------------------------------------------
> To unsubscribe, e-mail:
> For additional commands, e-mail:

Matt Sicker <>

  • Unnamed multipart/alternative (inline, None, 0 bytes)
View raw message