mirror of
https://github.com/idris-lang/Idris2.git
synced 2024-08-16 08:40:37 +03:00
Ignore 'docs/build'
This commit is contained in:
parent
f6e04b99ad
commit
d47202318a
2
.gitignore
vendored
2
.gitignore
vendored
@ -9,6 +9,8 @@
|
||||
|
||||
/build
|
||||
|
||||
/docs/build
|
||||
|
||||
/libs/**/build
|
||||
|
||||
/tests/**/build
|
||||
|
Loading…
Reference in New Issue
Block a user