diff --git a/library/.gitignore b/library/.gitignore
index 546197d23..d9a3e979b 100644
--- a/library/.gitignore
+++ b/library/.gitignore
@@ -1 +1,2 @@
-.lean_options
\ No newline at end of file
+.lean_options
+TAGS
\ No newline at end of file