Re: How to manage github pull requests?

On Fri, Dec 4, 2020 at 6:46 PM G. P. B. <george.banyard@gmail.com> wrote: > 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). > A semi automated version of this process can be seen at https://github.com/phpdocbrbridge/bridge . It's adapted for translations. André