Re: How to manage github pull requests?
| From: | G. P. B. | Date: | Fri, 04 Dec 2020 18:46:20 +0000 |
| Subject: | Re: How to manage github pull requests? | ||
| References: | 1 | Groups: | php.doc |
| Request: | Send a blank email to phpdoc+get-969387681@lists.php.net to get a copy of this message | ||
On Fri, 4 Dec 2020 at 18:43, Philip Olson <philip@roshambo.org> 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