diff options
| -rw-r--r-- | .gitignore | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore index 5264968e95..5339a0c44d 100644 --- a/.gitignore +++ b/.gitignore @@ -167,6 +167,7 @@ ide/index_urls.txt /user-contrib/* !/user-contrib/Ltac2 + .*.sw* .#* @@ -184,5 +185,6 @@ plugins/*/dune theories/*/dune theories/*/*/dune theories/*/*/*/dune +/user-contrib/Ltac2/dune *.install !Makefile.install |