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
commit8b8f84b0f0c107184a670f8a152b3b7a99796243 (patch)
tree8b013e6c3b9324a942f57a114bff929f5c251183 /src/sources
parent3f0f10c223ba86002f7c8af7c4dcd6d466f843f7 (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