Was it a large set of changes? I've seen this happen before where a large commit fails to sync to github. It's not a problem usually as the next commit usually triggers the mirror sync again and github "catches up".
On 5/11/18, 08:50, "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?
