diff --git a/.gitignore b/.gitignore index be86b80418edc5a9e6fdde46b4c8350b37c73a9c..017f06845bc9697055fe48db4d62460c772701d8 100644 --- a/.gitignore +++ b/.gitignore @@ -4,3 +4,4 @@ docker/Dockerfile doc/ext/__pycache__/ **__pycache__** _opam +*.vim