summaryrefslogtreecommitdiff
path: root/src/settings.sig
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adamc@hcoop.net>2010-01-03 15:58:34 -0500
committerGravatar Adam Chlipala <adamc@hcoop.net>2010-01-03 15:58:34 -0500
commit86bf1a00aacd96b4d32a1e1e88822a2201594926 (patch)
treeeeb16371c114308e706d86c6f9a03ddfbf0fa54f /src/settings.sig
parent6ee843295ea4449a5b8794db6880f8af7aaeff3e (diff)
Deadlines
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 12182ae6..f3a4379e 100644
--- a/src/settings.sig
+++ b/src/settings.sig
@@ -187,4 +187,7 @@ signature SETTINGS = sig
val setStaticLinking : bool -> unit
val getStaticLinking : unit -> bool
+ val setDeadlines : bool -> unit
+ val getDeadlines : unit -> bool
+
end