chore(.gitignore): ignore .md.lean files
Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
This commit is contained in:
parent
8b6421e4de
commit
73cd48cb13
1 changed files with 1 additions and 0 deletions
1
.gitignore
vendored
1
.gitignore
vendored
|
@ -2,6 +2,7 @@
|
||||||
.lean_trace
|
.lean_trace
|
||||||
*.produced.out
|
*.produced.out
|
||||||
*.md.lua
|
*.md.lua
|
||||||
|
*.md.lean
|
||||||
a.out
|
a.out
|
||||||
build
|
build
|
||||||
GPATH
|
GPATH
|
||||||
|
|
Loading…
Reference in a new issue