mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-09-11 13:36:08 +03:00
Ignore the root lib dir (#1278)
This commit is contained in:
parent
b65907f770
commit
d77c4f1fdf
2
.gitignore
vendored
2
.gitignore
vendored
@ -9,6 +9,8 @@
|
||||
|
||||
/build
|
||||
|
||||
/lib
|
||||
|
||||
idris2docs_venv
|
||||
/docs/build
|
||||
|
||||
|
Loading…
Reference in New Issue
Block a user