diff options
| author |  Adam Chlipala <adamc@hcoop.net> | 2010-02-11 09:10:01 -0500 |
|---|---|---|
| committer | Adam Chlipala <adamc@hcoop.net> | 2010-02-11 09:10:01 -0500 |
| commit | abe2d7ed6e151579cd6f13fd0ce92e29bb83a23d (patch) | |
| tree | 07742ac1accf17b7abc4153c890887c5a20ad464 /src/settings.sig | |
| parent | 861dbf0153f3383666dc0f3c35675d0b9a625b8d (diff) | |
sigfile directive
Diffstat (limited to 'src/settings.sig')
| -rw-r--r-- | src/settings.sig | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/settings.sig b/src/settings.sig index f3a4379e..348c47d4 100644 --- a/src/settings.sig +++ b/src/settings.sig @@ -96,7 +96,8 @@ signature SETTINGS = sig compile : string, (* Pass these `gcc -c' arguments *) linkStatic : string, (* Pass these static linker arguments *) linkDynamic : string,(* Pass these dynamic linker arguments *) - persistent : bool (* Multiple requests per process? *) + persistent : bool, (* Multiple requests per process? *) + code : unit -> Print.PD.pp_desc (* Extra code to include in C files *) } val addProtocol : protocol -> unit val setProtocol : string -> unit @@ -190,4 +191,7 @@ signature SETTINGS = sig val setDeadlines : bool -> unit val getDeadlines : unit -> bool + val setSigFile : string option -> unit + val getSigFile : unit -> string option + end |