summaryrefslogtreecommitdiff
path: root/src/sources
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2013-06-15 08:18:47 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2013-06-15 08:18:47 -0400
commit55889be0ddcf3426ba2c9ee4ddfca1998dde0e4f (patch)
tree8b013e6c3b9324a942f57a114bff929f5c251183 /src/sources
parent4445690a637c73f5b42d021622d404d932b3b684 (diff)
Add Sigcheck phase to avoid issues with signatures in global initializers
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 b49f0ba8..39360dd7 100644
--- a/src/sources
+++ b/src/sources
@@ -200,6 +200,9 @@ pathcheck.sml
sidecheck.sig
sidecheck.sml
+sigcheck.sig
+sigcheck.sml
+
cjr.sml
postgres.sig