Re: How to manage github pull requests?
André L F S Bacci <[email protected]>
| Newsgroups | gmane.comp.php.documentation.general |
|---|---|
| Message-ID | <CAL1T4B1D1Kkk0EXscHNoR9acbycfFG603nh_PQUFmhCyrdDZYg@mail.gmail.com> |
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é