diff options
| author |  Adam Chlipala <adam@chlipala.net> | 2010-10-14 11:35:56 -0400 |
|---|---|---|
| committer | Adam Chlipala <adam@chlipala.net> | 2010-10-14 11:35:56 -0400 |
| commit | 27bc339691e507e568c4ef10353dfeafe41b4a40 (patch) | |
| tree | 3e839cc2566526f3e4a294229c41f88e60e8d24e /src/settings.sml | |
| parent | ced024484333175eb138454309a9b6396f5a1f09 (diff) | |
-limit for running time
Diffstat (limited to 'src/settings.sml')
| -rw-r--r-- | src/settings.sml | 8 |
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 |