chore: add ignore = untracked
This commit is contained in:
parent
6b2303b243
commit
499449b66f
1 changed files with 3 additions and 2 deletions
5
.gitmodules
vendored
5
.gitmodules
vendored
|
|
@ -1,3 +1,4 @@
|
|||
[submodule "lake"]
|
||||
path = src/lake
|
||||
url = https://github.com/leanprover/lake.git
|
||||
path = src/lake
|
||||
url = https://github.com/leanprover/lake.git
|
||||
ignore = untracked
|
||||
Loading…
Add table
Reference in a new issue