Hello,

GitHub is currently experiencing problems <https://www.githubstatus.com/>; so far the one issue we saw ourselves is that Travis builds aren't triggered if a commit is pushed. This affects builds both for branches and pull requests; cron jobs may be fine.

@Committers: Please keep this in mind when merging things, as any issues on master will likely be detected later then usual.

Reply via email to