summaryrefslogtreecommitdiff
path: root/src/sources
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2009-04-16 14:49:25 -0400
committerGravatar Adam Chlipala <adamc@hcoop.net>2009-04-16 14:49:25 -0400
commit6d021ead0f73c5a28080b50a1bd08b1ab72590c9 (patch)
tree1560f6013ce6de0388180550168c20e9756eaa2c /src/sources
parent6d06bc0105d704373295c749aa65cc92488ac56c (diff)
Label exported symbols by effect-ness; factor out some common datatypes
Diffstat (limited to 'src/sources')
-rw-r--r--src/sources3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/sources b/src/sources
index 27b6673b..19e4e102 100644
--- a/src/sources
+++ b/src/sources
@@ -19,6 +19,9 @@ print.sml
prim.sig
prim.sml
+datatype_kind.sml
+export.sml
+
source.sml
urweb.grm