> On Dec 2, 2016, at 2:18 PM, Glyph Lefkowitz wrote:
>
> Hi all,
>
> On Github, the process was supposed to be that we push any 3rd-party
> contributor branches to the buildbots before doing a final merge. However,
> we (myself included, I think) have been landing PRs without doing that firs
Hi all,
On Github, the process was supposed to be that we push any 3rd-party
contributor branches to the buildbots before doing a final merge. However, we
(myself included, I think) have been landing PRs without doing that first.
In order to ensure that the process is followed, I've added a re