We now lint ALL files in the repository, not just those detected as changed in the commit (the procedure to do this failed when HEAD was exactly 1 commit ahead of the base branch). Also we now only lint pull requests, not in-progress pushes to any branch.