summaryrefslogtreecommitdiff
path: root/src/sources
diff options
context:
space:
mode:
authorGravatar Ziv Scully <ziv@mit.edu>2014-09-13 19:16:07 -0400
committerGravatar Ziv Scully <ziv@mit.edu>2014-09-13 19:16:07 -0400
commita7bfe57a2a355c5362d33e993394aa0bac300360 (patch)
tree1f81b256828f90ff34656d7d8fe703ce13d22e48 /src/sources
parent6b6635f390cc072971dcc7b37af00bca21c48364 (diff)
parent5d2d4930568267b0e205ece3d4908cdc7ff715a1 (diff)
Merge.
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 a87678f9..8860b310 100644
--- a/src/sources
+++ b/src/sources
@@ -229,6 +229,9 @@ $(SRC)/cjrize.sml
$(SRC)/scriptcheck.sig
$(SRC)/scriptcheck.sml
+$(SRC)/dbmodecheck.sig
+$(SRC)/dbmodecheck.sml
+
$(SRC)/prepare.sig
$(SRC)/prepare.sml