aboutsummaryrefslogtreecommitdiffhomepage
path: root/src/settings.sml
diff options
context:
space:
mode:
authorGravatar Ziv Scully <ziv@mit.edu>2015-11-19 17:29:47 -0500
committerGravatar Ziv Scully <ziv@mit.edu>2015-11-19 17:29:47 -0500
commit94b1dbce1ae20ded6b2e8cc519f56ac9e3b39b24 (patch)
treec9c4a9fe418a3634ce58f9e9c0a94180e924c1b5 /src/settings.sml
parent027ffcf5b2e3f71a42857547b17b0824d38a3f85 (diff)
Add consolidation heuristic options.
Diffstat (limited to 'src/settings.sml')
-rw-r--r--src/settings.sml4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/settings.sml b/src/settings.sml
index f9125c64..073e7883 100644
--- a/src/settings.sml
+++ b/src/settings.sml
@@ -811,6 +811,10 @@ val sqlcache = ref false
fun setSqlcache b = sqlcache := b
fun getSqlcache () = !sqlcache
+val sqlcacheHeuristic = ref "always"
+fun setSqlcacheHeuristic h = sqlcacheHeuristic := h
+fun getSqlcacheHeuristic () = !sqlcacheHeuristic
+
structure SM = BinaryMapFn(struct
type ord_key = string
val compare = String.compare