diff options
Diffstat (limited to 'packages.yaml')
| -rw-r--r-- | packages.yaml | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/packages.yaml b/packages.yaml index 04dd4cd4..f757cf99 100644 --- a/packages.yaml +++ b/packages.yaml @@ -757,6 +757,8 @@ filetypes: --- name: idris2 remote: edwinb/idris2-vim +ignored_dirs: +- doc filetypes: - name: idris2 extensions: |