Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
It looks like merging a pull request generates a push, so we shouldn't need to trigger this action on pull requests at all.
- Loading branch information