By default, the GitHub bot throttles commits being merged. In this case, it looks like multiple commits were landed right by each other due to manual merging (should only be done to fix this tree).

The build dashboard did not show this line of failures.

8988c4e was manually merged, so the previous commit failed to pick up.

This shouldn't happen. Moving to the webhook based approach would get rid of some of the complexity in the existing scheduler as we only need to schedule one commit at a time.