Using GitHub's merge button

Currently, our process [1] is to manually squash and commit pull requests.
This was discussed in the thread ending in [2]

As mentioned in the review of EME #165, it appears GitHub now supports
squashing via the big green button [3], and HTML now allows use of the
button [4]. I believe we can do the same thing.

As discussed in #165, there are still some details to figure out:

   - We need Philippe or someone else with admin access to verify both
   types are allowed in the GitHub repo settings [5].
   - Rebasing/merging: Rebasing might cause problems for history. (See the
   last paragraph below.) We might instead need to use merges when updating
   PRs. Either way, the squashed commit should be a single commit.
      - We might need to experiment here.
      - As an aside, it's helpful to the reviewer to delay rebasing/merging
      until the end.


The process will be approximately:

   - Push the green "Merge pull request" button.
   - Review and clean up the commit message.
   - Select "Confirm squash and merge"


Using the button should pretty much eliminate forced pushes, which can
cause diffs with comments to be lost as mentioned in #165.


[1] https://github.com/w3c/encrypted-media/blob/gh-pages/TEAM.md
[2] https://lists.w3.org/Archives/Public/public-html-media/2015Nov/0011.html
[3] https://github.com/blog/2141-squash-your-commits
[4] https://github.com/whatwg/html/blob/master/TEAM.md
[5]
https://help.github.com/articles/configuring-pull-request-merge-squashing/

Received on Thursday, 12 May 2016 17:14:38 UTC