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/