W3C home > Mailing lists > Public > public-html-media@w3.org > May 2016

Using GitHub's merge button

From: David Dorwin <ddorwin@google.com>
Date: Thu, 12 May 2016 10:13:51 -0700
Message-ID: <CAHD2rshckmzZAE6CD3tmCq2kSAj149G6qHL-SqZFigtt9vWbew@mail.gmail.com>
To: Mark Watson <watsonm@netflix.com>, Jerry Smith <jdsmith@microsoft.com>, Matt Wolenetz <wolenetz@google.com>, "public-html-media@w3.org" <public-html-media@w3.org>, Philippe Le H├ęgaret <plh@w3.org>
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
Received on Thursday, 12 May 2016 17:14:38 UTC

This archive was generated by hypermail 2.4.0 : Friday, 17 January 2020 15:49:08 UTC