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 506f1767..388e0996 100644
--- a/src/sources
+++ b/src/sources
@@ -119,6 +119,9 @@ mono_reduce.sml
mono_shake.sig
mono_shake.sml
+pathcheck.sigx
+pathcheck.sml
+
cjr.sml
cjr_env.sig