diff options
Diffstat (limited to '.gitignore')
-rw-r--r-- | .gitignore | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/.gitignore b/.gitignore index 948cd98d7..22f01e7c1 100644 --- a/.gitignore +++ b/.gitignore @@ -13,6 +13,27 @@ *.idx *.ilg *.toc +*.atoc +*.comidx +*.comind +*.erridx +*.errind +*.haux +*.hcomind +*.herrind +*.hind +*.htacind +*.htoc +*.ind +*.lof +*.tacidx +*.tacind +*.v.tex +*.v.pdf +*.v.ps +*.v.html +revision +TAGS bin/ config/Makefile config/coq_config.ml |