chore(library/.gitignore): add TAGS
This commit is contained in:
parent
6911cb0af0
commit
76d310da8b
1 changed files with 2 additions and 1 deletions
3
library/.gitignore
vendored
3
library/.gitignore
vendored
|
@ -1 +1,2 @@
|
|||
.lean_options
|
||||
.lean_options
|
||||
TAGS
|
Loading…
Reference in a new issue