New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Add bot usernames for idris-lang/idris-dev #16

sagesharp opened this Issue Nov 8, 2016 · 0 comments


None yet
1 participant

sagesharp commented Nov 8, 2016

Many github communities use bots to suggest reviewers, do automated testing, and more.

foss-heartbeat breaks bots into a separate category in the html contribution statistics, by checking for the username in getBots in

Additionally, if a bot merges a commit after being issued a command in a pull request comment, appendReviewers in will attribute the merge to that person, as well as to the bot. Currently, we check for a specific command string at the beginning of the comment. If your test-and-merge bot accepts commands in the middle of a comment, please update the code.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment