diff options
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 |