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.
Locked
