Ignore idris2 doc, fixes #538

This commit is contained in:
Adam Stankiewicz
2020-09-06 02:34:46 +02:00
parent 3baafd5c33
commit 57badea2dc
2 changed files with 2 additions and 158 deletions

View File

@@ -757,6 +757,8 @@ filetypes:
---
name: idris2
remote: edwinb/idris2-vim
ignored_dirs:
- doc
filetypes:
- name: idris2
extensions: