From 80839a44f1752669c8c4e0de440b1e49ba909aeb Mon Sep 17 00:00:00 2001
From: David Robertson <davidr@element.io>
Date: Sun, 3 Apr 2022 21:21:08 +0100
Subject: Remove more dead/broken dev scripts (#12355)

---
 mypy.ini | 3 ---
 1 file changed, 3 deletions(-)

(limited to 'mypy.ini')

diff --git a/mypy.ini b/mypy.ini
index 85291099ac..ac2a5c753d 100644
--- a/mypy.ini
+++ b/mypy.ini
@@ -24,11 +24,8 @@ files =
 exclude = (?x)
   ^(
    |scripts-dev/build_debian_packages.py
-   |scripts-dev/definitions.py
    |scripts-dev/federation_client.py
-   |scripts-dev/hash_history.py
    |scripts-dev/release.py
-   |scripts-dev/tail-synapse.py
 
    |synapse/_scripts/export_signing_key.py
    |synapse/_scripts/move_remote_media_to_new_store.py
-- 
cgit 1.4.1