Re: How to manage github pull requests?

Hello,

> On Dec 4, 2020, at 10:57 AM, André L F S Bacci <[email protected]> wrote:
> 
> On Fri, Dec 4, 2020 at 6:46 PM G. P. B. <[email protected]> wrote:
> 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).
> 
> A semi automated version of this process can be seen at https://github.com/phpdocbrbridge/bridge . It's adapted for translations.
> 
> André

Thanks but I remain a bit confused and am looking for the simplest method 
possible. Also I'm an old timer that's completely unaware of the doc's git/svn 
status.

In looking here:
  https://qa.php.net/pulls/#repo=doc-en

It references instructions, do we follow them? What about the commit (sync)
to SVN, is that automated? The above does not reference SVN as I assume
the tool is more specific to the github<->git.php.net process as few php.net 
projects use SVN.

Today is the first time I've seen this (doc repos on git.php.net) too:
  http://git.php.net/?p=doc/en.git;a=summary

So do we commit the PR there first then manually get that change into svn.php.net? 
Ideally there's a nice way that tracks the PR (original author) to SVN.

Regards,
Philip