diff options
author | Adam Chlipala <adam@chlipala.net> | 2016-03-12 14:11:27 -0500 |
---|---|---|
committer | Adam Chlipala <adam@chlipala.net> | 2016-03-12 14:11:27 -0500 |
commit | 6b85dbb54d5d9928a53f0f916cf0cb33c04ff87c (patch) | |
tree | 0215bd5985818f74a20c8bc37867e7ee234b0570 /src/sources | |
parent | d2823e60805a6cc394b149563ff500ea969b8627 (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/sources | 6 |
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 |