summaryrefslogtreecommitdiff
path: root/src/compiler.sig
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-02-11 09:10:01 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-02-11 09:10:01 -0500
commitabe2d7ed6e151579cd6f13fd0ce92e29bb83a23d (patch)
tree07742ac1accf17b7abc4153c890887c5a20ad464 /src/compiler.sig
parent861dbf0153f3383666dc0f3c35675d0b9a625b8d (diff)
sigfile directive
Diffstat (limited to 'src/compiler.sig')
-rw-r--r--src/compiler.sig3
1 files changed, 2 insertions, 1 deletions
diff --git a/src/compiler.sig b/src/compiler.sig
index fd1eccf8..78e82ba8 100644
--- a/src/compiler.sig
+++ b/src/compiler.sig
@@ -51,7 +51,8 @@ signature COMPILER = sig
filterUrl : Settings.rule list,
filterMime : Settings.rule list,
protocol : string option,
- dbms : string option
+ dbms : string option,
+ sigFile : string option
}
val compile : string -> bool
val compiler : string -> unit