Add gtags files to .gitignore
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
1448dd5098
commit
d72f24a5e5
1 changed files with 5 additions and 1 deletions
4
.gitignore
vendored
4
.gitignore
vendored
|
@ -2,3 +2,7 @@
|
||||||
.lean_trace
|
.lean_trace
|
||||||
a.out
|
a.out
|
||||||
build
|
build
|
||||||
|
GPATH
|
||||||
|
GRTAGS
|
||||||
|
GSYMS
|
||||||
|
GTAGS
|
Loading…
Reference in a new issue