diff options
| author | Vincent Laporte | 2019-05-09 12:44:28 +0000 |
|---|---|---|
| committer | Vincent Laporte | 2019-05-09 12:50:32 +0000 |
| commit | 66df9050edb8c1fe10992a58f2ec51957cf03449 (patch) | |
| tree | 969be39526738aceef400ce634dbf7dc3dd7162f /.gitignore | |
| parent | b2826206063c1ce596736a1e92550b4c24eaea71 (diff) | |
Ignore generated dune file for Ltac2
Diffstat (limited to '.gitignore')
| -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 |