summaryrefslogtreecommitdiff
path: root/.hgignore
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2011-11-05 15:05:13 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2011-11-05 15:05:13 -0400
commit2818af2ec6161b85d1cfcbd77d9ea965ae40025c (patch)
treebb624710b05d07871646fc5a93a9b7014d5874dd /.hgignore
parentb3c3e4d97eebb1cae5b53213a2d9ebfc7d071c4e (diff)
Support the full set of XHTML character entities
Diffstat (limited to '.hgignore')
-rw-r--r--.hgignore3
1 files changed, 3 insertions, 0 deletions
diff --git a/.hgignore b/.hgignore
index cfb45564..401353b3 100644
--- a/.hgignore
+++ b/.hgignore
@@ -48,6 +48,9 @@ doc/*.html
Makefile.coq
*.vo
+xml/parse
+xml/entities.sml
+
syntax: regexp
^Makefile$