chore(library/.gitignore): update
This commit is contained in:
parent
e966aa3145
commit
226f301044
1 changed files with 4 additions and 2 deletions
6
library/.gitignore
vendored
6
library/.gitignore
vendored
|
@ -1,2 +1,4 @@
|
||||||
.lean_options
|
TAGS
|
||||||
TAGS
|
build.ninja
|
||||||
|
.ninja_deps
|
||||||
|
.ninja_log
|
||||||
|
|
Loading…
Reference in a new issue