- From: Sangwhan Moon <sangwhan@iki.fi>
- Date: Fri, 28 Mar 2014 14:41:01 +0900
- To: "public-webevents@w3.org" <public-webevents@w3.org>
Reopened as: https://github.com/w3c/web-platform-tests/pull/806 -- Sangwhan Moon On Friday, March 28, 2014 at 12:45, Sangwhan Moon wrote: > 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 05:41:38 UTC