Since github is a popular source of activity, here are two things to know for developers on the receiving end:
* If you don't have one, make a github account. * To get notifications you should watch the GH mirror of our repo, go to http://github.com/plt/racket and click the "Watch" button. (There was some confusion with starring -- Matthew reported that starring by itself doesn't get you the notifications.) * You should now get email notifications about pull requests. When a pull request looks relevant, the email will have two relevant URLs -- the main one is where you can go to see the pull, something like this: https://github.com/plt/racket/pull/198 You get to the default "discussion" tab, and you can click the "commits" to see the list of commits, and "files changed" to see the changes. You should review both the changes and see that the commits look fine. (For example, every once in a while people will not rebase their tree before submitting a pull request, which results in a pull request that has a bunch of commits that are already in our repo.) The other important URL is the same as the above, but with an extra ".patch" in the end: https://github.com/plt/racket/pull/198.patch This is in the same email format that git knows how to deal with, so you can simply pipe this into "git am": curl https://github.com/plt/racket/pull/198.patch | git am After that's done, you will have the commits in your repository, and you can now push as usual (and do a "pull --rebase" before that if needed). * Note that before you push, the commits will have the original author name & date but you will be the committer. Before you push, you can do the usual history editing if you want to clean things up. For example, if the pull had N commits that are all doing a single thing, it is a good idea to squash them into a single commit, and/or edit the commit message, or maybe you see some typo in the pull but since it's a small thing you want to combine your fix with the received commits (in which case it's probably best to have some note about it in the combined commit message). All of these are perfectly safe to do -- and the original author name is still going to be preserved, so there's no loss of hacking credit. That should be the case even if you squash your own commit with the received commits. (You can check that before pushing, of course.) * Finally, the pull request needs to be closed. Unfortunately, the only people who can close pull request are the submitter and me[*]. The easiest thing to do is to add a comment that says that the commit was merged -- either I'll see that and close it, or the submitter will. Note that the github notifications are reply-able, which means that you can simply send a reply to the original notification with a "merged, thanks" text, which I'll see. [*] The reason for that is something that I mentioned not too long ago: github has some system to specify people with read or write access, and to be able to close issues and pull requests you need the latter. The problem is that giving you write access means that you can actually push changes to our github repo -- but the next push to our server will cause a followup (forced) push to the github mirror which will obliterate your push. So in theory, I obviously have no problems giving you write access, but in practice I worry about people doing some mistake and ending up with a messed repository and worse, with a bunch of work that went up in virtual smoke. I did ask them to add a separate capability to manage issues, and the reply I got (in April) was: | You're right that the permissions are limited, but they're the | ones currently available. I'll add your description of a new type | of permissions as a feature request, and show the team. I didn't hear anything else about it, so I don't know if they'll add it or not. Feel free to nag them... -- ((lambda (x) (x x)) (lambda (x) (x x))) Eli Barzilay: http://barzilay.org/ Maze is Life! _________________________ Racket Developers list: http://lists.racket-lang.org/dev