summaryrefslogtreecommitdiff
path: root/src/sources
diff options
context:
space:
mode:
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