Hello, On Sun, 25 Jun 2017 10:33:20 +0200 Antoine Pitrou <solip...@pitrou.net> wrote:
[] > Hmm. If it were so easy, you wouldn't have felt the need to add that > functionality to blurb, right? :-) > > This is touching a more general problem, though. Before GitHub, we > (core developers) would take the patch submitted by a contributor, > make whatever minor changes were needed (e.g. Misc/NEWS) and push the > aggregate ourselves. With GitHub, while it's possible to edit someone > else's PR, it's frankly a PITA (I've tried to do it once, I don't want > to try a second time unless GitHub makes it massively easier and less > footgunning-prone). Sorry, but how that can be true? A GitHub PR is just a git branch (in somebody else's repository, but also in the repository it's submitted to). So, like any git branch, you can fetch it, re-branch to your local branch, apply any changes to it, rebase, push anywhere. There're also various tools for dealing specifically with git branch layout as used by Github, and every real man writes their own (because it's easier to shoot a 5-liner than to review whether somebody else's tool do what you need or not, it's all trivial git commands anyway). [] -- Best regards, Paul mailto:pmis...@gmail.com _______________________________________________ Python-Dev mailing list Python-Dev@python.org https://mail.python.org/mailman/listinfo/python-dev Unsubscribe: https://mail.python.org/mailman/options/python-dev/archive%40mail-archive.com
