summaryrefslogtreecommitdiff
path: root/src/sources
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 /src/sources
parent22d36c8605e1d006a379350e28a5f939f7082546 (diff)
Support the full set of XHTML character entities
Diffstat (limited to 'src/sources')
-rw-r--r--src/sources5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/sources b/src/sources
index ebc2ab13..862845d5 100644
--- a/src/sources
+++ b/src/sources
@@ -47,6 +47,11 @@ export.sml
source.sml
+utf8.sig
+utf8.sml
+
+../xml/entities.sml
+
urweb.grm
urweb.lex