summaryrefslogtreecommitdiff
path: root/src/settings.sig
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2016-01-02 10:44:03 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2016-01-02 10:44:03 -0500
commitd47ffbc86c1cafb041588ab0ea7540c538196cb9 (patch)
treebb4af40404463ab02504a0bc219d994bed28ad7a /src/settings.sig
parentaa3e615e84e3e8844fd5537ef84c38d5d18298ab (diff)
parent2db6f2680dc91cd32b7c76e354bc39fe5192c857 (diff)
Merge branch 'master' of ssh://github.com/urweb/urweb
Diffstat (limited to 'src/settings.sig')
-rw-r--r--src/settings.sig3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/settings.sig b/src/settings.sig
index 732a31fa..c75f12a3 100644
--- a/src/settings.sig
+++ b/src/settings.sig
@@ -238,6 +238,9 @@ signature SETTINGS = sig
val setStaticLinking : bool -> unit
val getStaticLinking : unit -> bool
+ val setBootLinking : bool -> unit
+ val getBootLinking : unit -> bool
+
val setDeadlines : bool -> unit
val getDeadlines : unit -> bool