summaryrefslogtreecommitdiff
path: root/src/settings.sml
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2010-10-14 11:35:56 -0400
committerGravatar Adam Chlipala <adam@chlipala.net>2010-10-14 11:35:56 -0400
commit27bc339691e507e568c4ef10353dfeafe41b4a40 (patch)
tree3e839cc2566526f3e4a294229c41f88e60e8d24e /src/settings.sml
parentced024484333175eb138454309a9b6396f5a1f09 (diff)
-limit for running time
Diffstat (limited to 'src/settings.sml')
-rw-r--r--src/settings.sml8
1 files changed, 6 insertions, 2 deletions
diff --git a/src/settings.sml b/src/settings.sml
index 4512b7d8..b5ba4f9b 100644
--- a/src/settings.sml
+++ b/src/settings.sml
@@ -492,12 +492,16 @@ fun getOnError () = !onError
val limits = ["messages", "clients", "headers", "page", "heap", "script",
"inputs", "subinputs", "cleanup", "deltas", "transactionals",
- "globals", "database"]
+ "globals", "database", "time"]
val limitsList = ref ([] : (string * int) list)
fun addLimit (v as (name, _)) =
if List.exists (fn name' => name' = name) limits then
- limitsList := v :: !limitsList
+ (limitsList := v :: !limitsList;
+ if name = "time" then
+ setDeadlines true
+ else
+ ())
else
raise Fail ("Unknown limit category '" ^ name ^ "'")
fun limits () = !limitsList