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
commit60dfbfbc250c197357d84771bdc5aaaa812c573e (patch)
treeeeb16371c114308e706d86c6f9a03ddfbf0fa54f /src/settings.sig
parentf1498d6ff5dfe5c210bfa0492da5a8b8414efc1a (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