No, it was probably 5k-10kb of updates. On Fri, May 11, 2018 at 8:59 AM Marc Parisi <[email protected]> wrote:
> I've seen it get stuck only to unstick with another merge > > On Fri, May 11, 2018, 8:50 AM Mike Thomsen <[email protected]> wrote: > > > I approved one of Matt's PRs and merged, but it seems to be taking > > unusually long for the sync to GitHub. Is something broken? > > >
