summaryrefslogtreecommitdiff
path: root/.hgignore
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2008-11-27 14:38:53 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2008-11-27 14:38:53 -0500
commit85a682b4a65a76e2f5a120b28faf7093f4a766a9 (patch)
tree3f180b88f47fe8cfb1f6dda748baf30d41363b56 /.hgignore
parent9004ba508ee89c4fe4b758ffe0f87518b48670ae (diff)
Start of manual
Diffstat (limited to '.hgignore')
-rw-r--r--.hgignore7
1 files changed, 6 insertions, 1 deletions
diff --git a/.hgignore b/.hgignore
index b388b26a..fe5b6659 100644
--- a/.hgignore
+++ b/.hgignore
@@ -13,7 +13,7 @@ src/urweb.mlb
*.grm.*
*.o
-Makefile
+./Makefile
src/config.sml
*.exe
@@ -27,3 +27,8 @@ demo/demo.*
*.sql
*mlmon.out
+
+*.aux
+*.dvi
+*.pdf
+*.ps