From d6bbc939b2e7c52a4c33b6a2922858c2312f9d7a Mon Sep 17 00:00:00 2001
From: Robin van Boven <497556+Beanow@users.noreply.github.com>
Date: Thu, 19 Sep 2019 17:52:20 +0200
Subject: [PATCH] Add more bots. (#1383)

Fixes #1381
---
 src/plugins/github/bots.js | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/src/plugins/github/bots.js b/src/plugins/github/bots.js
index 916a2f3..0923947 100644
--- a/src/plugins/github/bots.js
+++ b/src/plugins/github/bots.js
@@ -5,9 +5,11 @@
 export function botSet(): Set<string> {
   return new Set([
     "codecov",
+    "codecov-io",
     "credbot",
     "facebook-github-bot",
     "gitcoinbot",
+    "gitter-badger",
     "googlebot",
     "greenkeeper",
     "greenkeeperio-bot",