Not a real question, rather a suggestion if anyone has faced the same needs.
Suppose to have a github repository with many contributors making PR. What are the best tools to automatic merge PR with the following condition:
- in there is no activity for a while (e.g. 10 days) close the PR without merging it IF the author has NOT commit rights on the repo and merge it IF the author has commit rights
I found several useful tool, like github APP:
- bulldozer that merges PR based on conditions (but not time intervals)
- policy-bot that tags the PR as approved/not approved depending on some conditions
- mergify that auto merges PR depending on different conditions (again, no time intervals)
- writing a webhook?
In some ways I think that a synergy between APPs and other tools can solve the problem, but maybe there is a smoother way to do this.
Someone has some suggestions?