summaryrefslogtreecommitdiff
path: root/src/sources
diff options
context:
space:
mode:
authorGravatar Benjamin Barenblat <bbaren@mit.edu>2018-06-17 09:12:52 -0400
committerGravatar Benjamin Barenblat <bbaren@mit.edu>2018-06-17 09:12:52 -0400
commit095c2640aa2070ed4e2765875238d5e6e6673856 (patch)
tree9306beb3fef29a99d9436dc00e2d8c57fb3e0c7b /src/sources
parent8c58ba2e1db6e97ca1f18fd9ca52ffead53e4a4f (diff)
parent34eb9eba9a724433f9c37c39cf43e9e10cf55220 (diff)
Merge branch 'upstream' into dfsg_clean20180616+dfsg
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 52b1bdd7..5c0b2a84 100644
--- a/src/sources
+++ b/src/sources
@@ -231,6 +231,9 @@ $(SRC)/sidecheck.sml
$(SRC)/sigcheck.sig
$(SRC)/sigcheck.sml
+$(SRC)/filecache.sig
+$(SRC)/filecache.sml
+
$(SRC)/mono_inline.sml
$(SRC)/sha1.sig