From 13780bcee51f870c02d3a5b248db218ac0ea5bd6 Mon Sep 17 00:00:00 2001
From: leanprover-community-bot <leanprover.community@gmail.com>
Date: Tue, 21 Sep 2021 02:39:51 +0000
Subject: [PATCH] chore(scripts): update nolints.txt (#9317)

I am happy to remove some nolints for you!
---
 scripts/nolints.txt | 9 ---------
 1 file changed, 9 deletions(-)

diff --git a/scripts/nolints.txt b/scripts/nolints.txt
index 260eb98a07930..fef487a239ec1 100644
--- a/scripts/nolints.txt
+++ b/scripts/nolints.txt
@@ -355,15 +355,6 @@ apply_nolint wseq.mem doc_blame
 apply_nolint wseq.tail.aux doc_blame
 apply_nolint wseq.think_congr unused_arguments
 
--- data/vector/basic.lean
-apply_nolint vector.insert_nth doc_blame
-apply_nolint vector.m_of_fn doc_blame
-apply_nolint vector.mmap doc_blame
-apply_nolint vector.reverse doc_blame
-apply_nolint vector.to_array doc_blame
-apply_nolint vector.traverse doc_blame
-apply_nolint vector.traverse_def unused_arguments
-
 -- data/vector3.lean
 apply_nolint vector3 has_inhabited_instance
 apply_nolint vector3.cons_elim doc_blame