summaryrefslogtreecommitdiff
path: root/src/settings.sig
diff options
context:
space:
mode:
Diffstat (limited to 'src/settings.sig')
-rw-r--r--src/settings.sig6
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