Re: How to manage github pull requests?

On Fri, 4 Dec 2020 at 18:43, Philip Olson <[email protected]> wrote:

> Hi all,
>
> 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 :)
>
> Regards,
> Philip
>

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).

Hope this helps,

Best regards,

George P. Banyard