summaryrefslogtreecommitdiff
path: root/.hgignore
diff options
context:
space:
mode:
Diffstat (limited to '.hgignore')
-rw-r--r--.hgignore4
1 files changed, 4 insertions, 0 deletions
diff --git a/.hgignore b/.hgignore
index 4e578224..c0222189 100644
--- a/.hgignore
+++ b/.hgignore
@@ -33,3 +33,7 @@ demo/demo.*
*.pdf
*.ps
*.toc
+
+.depend
+Makefile.coq
+*.vo