From 101049de2727462436c0b84de29d870c6faded6b Mon Sep 17 00:00:00 2001
From: Aman Agrawal <f2016561@pilani.bits-pilani.ac.in>
Date: Tue, 6 Aug 2019 07:54:54 +0530
Subject: [PATCH] lint: Add mypy as an external_linter to be run with
 ./tools/lint.

We were not running `mypy` with `./tools/lint` prior to this.
---
 tools/lint | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/tools/lint b/tools/lint
index 28ba647..0d69fa3 100755
--- a/tools/lint
+++ b/tools/lint
@@ -25,6 +25,9 @@ def run():
     by_lang = linter_config.list_files(file_types=['py', 'sh', 'json', 'md', 'txt'],
                                        exclude=EXCLUDED_FILES)
 
+    linter_config.external_linter('mypy', ['tools/run-mypy'], ['py'], pass_targets=False,
+                                  description="Static type checker for Python (config: mypy.ini)")
+
     @linter_config.lint
     def custom_py():
         # type: () -> int