chore(.gitignore): add .lean_options
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
f555c9916e
commit
464f991eba
1 changed files with 1 additions and 0 deletions
1
.gitignore
vendored
1
.gitignore
vendored
|
@ -18,5 +18,6 @@ Makefile
|
|||
CMakeFiles/
|
||||
.projectile
|
||||
.coveralls.yml
|
||||
.lean_options
|
||||
doc/html
|
||||
make.deps
|
Loading…
Reference in a new issue