- From: Sangwhan Moon <sangwhan@iki.fi>
- Date: Fri, 28 Mar 2014 12:45:49 +0900
- To: Scott González <scott.gonzalez@gmail.com>
- Cc: Arthur Barstow <art.barstow@nokia.com>, "public-webevents@w3.org" <public-webevents@w3.org>
On Thursday, March 27, 2014 at 22:07, Scott González wrote: > On Thu, Mar 27, 2014 at 6:33 AM, Sangwhan Moon <sangwhan@iki.fi (mailto:sangwhan@iki.fi)> wrote: > > Thanks, just don't delete the branch. :-) > > > Pull requests are permanent records. Even if the original branch is deleted, the commits will live indefinitely on GitHub. That's good to know. I wasn't so sure since pull requests aren't a standard git feature. (I use git every day, but very rarely use GitHub.) > > > > > It might require reopening the PR under my account (not sure how this works in GH) - I'll ask around > > > > on what the standard procedure for this is. > > > > > > > You can just pull the branch locally, add your commits, push to a branch on your GitHub account and send a new pull request. The original commits will still have the correct author information. Yes, I am aware of this approach - but it's bit cruft for no gain. I was more curious about "is there a better way" or is there a more "size efficient way" to do this. Asking around and some searching says what I want is a big fat "nope". It should be possible to systematically re-assign or steal ownership of PRs, since people may not (or may not be able to) follow up on a PR they sent a year ago, and there is nothing technical that blocks this, except GitHub it seems. :-)
Received on Friday, 28 March 2014 03:46:25 UTC