merging PRs on github (was Re: [pure-data/pure-data] keybinding for CapsLock cases (same as without CapsLock) (#61))
(taking this off the github issue, since it's unrelated)
On 06/30/2017 09:40 AM, Dan Wilcox wrote:
(personally, I hardly ever use the merge button, because I want to test the merged code locally before publishing it)
You can add the submitters repo locally as a remote, fetch the remote branch, then checkout and test. If things are good, you hit the Github Merge button which handles all the rest. This has worked well for me in the past.
obviously there are a number of different workflows. this is what i like about git.
in any case: i, personally, find it tedious to have to switch back to the github webpage just to press the merge button when i can as well do a `git push`. (i've had a number of PRs that required some extra work after merge; doing it myself was way more energy-preserving than trying to get the committer fix the PR so it was 100% perfect)
merging locally and then doing `git push` is also one of the officially documented ways to *properly* merge a PR. (just go to a random PR where you have merge-priviliges; and click on "view command line instruction" besides the "Merge pull request" button). if this doesn't properly make the PR show up as "merged", then we've hit a bug at github and should report it (rather than adapt our workflows).
and then, there's always the chance that the PR doesn't actually apply cleanly any more (as was the case with PR#61), and applying it actually requires a re-write (as miller has done; and he was simply faster than me, who hadn't even noticed that the PR would no longer apply), thus making it impossible for github to automatically detect the merge.
i really think that this is an edge case, and that we really don't need any special action (to change whatever workflow one prefers).
gfma IOhannes
Speaking only for myself... so far I've been investigating PRs in th following way: (1) look at teh diffs as the website shows them to try to understand what the changes are about and then either (2a) fetching the PR and trying to merge it into my private repo; or (2b) rewriting the whole thing by hand (as in https://github.com/pure-data/pure-data/pull/66 which turned out to be a band-aid on some code that really needed more work) or (2c) cherry-picking some but not all of the commits using "git AM".
In some of these cases I think it would have been easier to operate on a clone of the github repo; in others I think there's little way I could improve on my dumb way of doing it :)
M
On Fri, Jun 30, 2017 at 08:37:24PM +0200, IOhannes m zmölnig wrote:
(taking this off the github issue, since it's unrelated)
On 06/30/2017 09:40 AM, Dan Wilcox wrote:
(personally, I hardly ever use the merge button, because I want to test the merged code locally before publishing it)
You can add the submitters repo locally as a remote, fetch the remote branch, then checkout and test. If things are good, you hit the Github Merge button which handles all the rest. This has worked well for me in the past.
obviously there are a number of different workflows. this is what i like about git.
in any case: i, personally, find it tedious to have to switch back to the github webpage just to press the merge button when i can as well do a `git push`. (i've had a number of PRs that required some extra work after merge; doing it myself was way more energy-preserving than trying to get the committer fix the PR so it was 100% perfect)
merging locally and then doing `git push` is also one of the officially documented ways to *properly* merge a PR. (just go to a random PR where you have merge-priviliges; and click on "view command line instruction" besides the "Merge pull request" button). if this doesn't properly make the PR show up as "merged", then we've hit a bug at github and should report it (rather than adapt our workflows).
and then, there's always the chance that the PR doesn't actually apply cleanly any more (as was the case with PR#61), and applying it actually requires a re-write (as miller has done; and he was simply faster than me, who hadn't even noticed that the PR would no longer apply), thus making it impossible for github to automatically detect the merge.
i really think that this is an edge case, and that we really don't need any special action (to change whatever workflow one prefers).
gfma IOhannes
Pd-dev mailing list Pd-dev@lists.iem.at https://lists.puredata.info/listinfo/pd-dev
-
IOhannes m zmölnig -
Miller Puckette