Re: How to manage github pull requests?

On 04.12.2020 at 19:46, G. P. B. wrote: > On Fri, 4 Dec 2020 at 18:43, Philip Olson <philip@roshambo.org> wrote: > >> 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 :) > > 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). Yes, that is the recommended way. To my knowledge, directly merging in Git is possible, but that screws up existing checkouts and PRs. Also, when "merging" PR #12345, for instance, add Closes GH-12345. to the end of the commit message. That automatically closes the respective PR, and adds a notice including the Git commit hash. Regards, Christoph