Discriminate pull request events #5
Description
Not every pull request event from GitHub is created equal. Some are relevant to the mergeability of pull requests and some are not. For instance, editing the title or description of the pull request will initiate an event from GitHub. This is a useful event to some, but not for us. It should not initiate another merge process. There are no new commits to analyze, so it seems like a waste of resources to initiate a new integration.
If a label is added to a PR or someone requests a code review, then it should also be ignored.
GitHub's API has an action field for describing the types of PR actions:
- assigned
- unassigned
- review_requested
- review_request_removed
- labeled
- unlabeled
- opened
- edited
- closed
- reopened
It's not clear how to understand if the commits have changed from the above.
However, one benefit of this defect is that it does offer a manner to initiate the merge process again. This might be useful if there was a defect in this merging application, or there was a transient error (network issue, failure to retrieve pull request information or Git commits, and so on). So this may be a feature and not a bug.