summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2018-06-03 15:05:39 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2018-06-03 15:05:39 -0400
commit50010c982776ae62233f577f74a8e92e02c5b190 (patch)
treef994a1325d754b2b164cc2c5a3dd3054183e49d9
parentf3373fd5809689bece7fd390f2d737aa0b43f594 (diff)
Fail when requesting a file cache with a database engine that won't do SHA512
-rw-r--r--src/settings.sml7
1 files changed, 6 insertions, 1 deletions
diff --git a/src/settings.sml b/src/settings.sml
index 47a88932..cfbe98a5 100644
--- a/src/settings.sml
+++ b/src/settings.sml
@@ -727,7 +727,12 @@ fun setSigFile v = sigFile := v
fun getSigFile () = !sigFile
val fileCache = ref (NONE : string option)
-fun setFileCache v = fileCache := v
+fun setFileCache v =
+ (if Option.isSome v andalso not (#supportsSHA512 (currentDbms ())) then
+ ErrorMsg.error "The selected database engine is incompatible with file caching."
+ else
+ ();
+ fileCache := v)
fun getFileCache () = !fileCache
structure SS = BinarySetFn(struct