summaryrefslogtreecommitdiff
path: root/src/sources
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2016-03-12 14:11:27 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2016-03-12 14:11:27 -0500
commit6b85dbb54d5d9928a53f0f916cf0cb33c04ff87c (patch)
tree0215bd5985818f74a20c8bc37867e7ee234b0570 /src/sources
parentd2823e60805a6cc394b149563ff500ea969b8627 (diff)
Sqlcache: also record script additions; do a MonoReduce afterward, to help Prepare do a better job
Diffstat (limited to 'src/sources')
-rw-r--r--src/sources6
1 files changed, 3 insertions, 3 deletions
diff --git a/src/sources b/src/sources
index 8bf80bc6..1a09e7e8 100644
--- a/src/sources
+++ b/src/sources
@@ -186,9 +186,6 @@ $(SRC)/cache.sml
$(SRC)/toy_cache.sml
$(SRC)/lru_cache.sml
-$(SRC)/sqlcache.sig
-$(SRC)/sqlcache.sml
-
$(SRC)/monoize.sig
$(SRC)/monoize.sml
@@ -210,6 +207,9 @@ $(SRC)/fuse.sml
$(SRC)/iflow.sig
$(SRC)/iflow.sml
+$(SRC)/sqlcache.sig
+$(SRC)/sqlcache.sml
+
$(SRC)/name_js.sig
$(SRC)/name_js.sml