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
commit61bd40e1af8c3f7ace2a09068557ac7c05662b69 (patch)
tree3f180b88f47fe8cfb1f6dda748baf30d41363b56 /.hgignore
parentdf08dfc3be26b2cf829a1ea31b63f4aaecf1f3bf (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