summaryrefslogtreecommitdiff
path: root/src/shake.sig
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-01-03 12:47:27 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-01-03 12:47:27 -0500
commit9890b6de2e6877c67650f64410127ee2dfe8581e (patch)
tree784c36f589cbacce89a4ab23334fda77871e7961 /src/shake.sig
parentd777d7da78fccb8f15eccff680deca36ae57314b (diff)
Proper C-side deserialization; Shake.sliceDb
Diffstat (limited to 'src/shake.sig')
-rw-r--r--src/shake.sig3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/shake.sig b/src/shake.sig
index 6c617435..2b805dea 100644
--- a/src/shake.sig
+++ b/src/shake.sig
@@ -31,4 +31,7 @@ signature SHAKE = sig
val shake : Core.file -> Core.file
+ val sliceDb : bool ref
+ (* Set this to try to delete anything not needed to determine the database schema. *)
+
end