summaryrefslogtreecommitdiff
path: root/src/shake.sig
diff options
context:
space:
mode:
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