Re: How to manage github pull requests?

On 04.12.2020 at 19:46, G. P. B. wrote:

> On Fri, 4 Dec 2020 at 18:43, Philip Olson <[email protected]> wrote:
>
>> How do we merge github pull requests into the documentation? Or more
>> specifically,
>> what's the official procedure to merge them into SVN? I see git-svn-id
>> exists but
>> am unsure how exactly it's generated.
>>
>> All thoughts are welcome, thanks :)
>
> If add .diff at the end of GitHub PR URL it will redirect you to the diff
> patch for the PR.
> You should then be able to cURL that URL and pipe it into `patch -p0` to
> apply it
> (this assumes you are in the 'en' folder and not at the root of the SVN
> docs tree).

Yes, that is the recommended way.  To my knowledge, directly merging in
Git is possible, but that screws up existing checkouts and PRs.

Also, when "merging" PR #12345, for instance, add

  Closes GH-12345.

to the end of the commit message.  That automatically closes the
respective PR, and adds a notice including the Git commit hash.

Regards,
Christoph