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
commit954936dd180e34b79baca71e43d55a204dda9594 (patch)
treebb624710b05d07871646fc5a93a9b7014d5874dd /.hgignore
parent22d36c8605e1d006a379350e28a5f939f7082546 (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$