diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-05-27 14:41:47 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-05-27 14:41:47 -0400 |
| commit | 9006b759cfa01c6006196e0716c2d67c760556a6 (patch) | |
| tree | 6870500d18b75d7464b4b5c910ff2edf186a8db0 /src/main/options | |
| parent | a891d1259fb3d250910186bbdf3083b55eb23f26 (diff) | |
timespec printing bug
Diffstat (limited to 'src/main/options')
| -rw-r--r-- | src/main/options | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/main/options b/src/main/options index 8733011f7..943f46b61 100644 --- a/src/main/options +++ b/src/main/options @@ -53,4 +53,7 @@ undocumented-alias --segv-nospin = --no-segv-spin expert-option waitToJoin --wait-to-join bool :default true wait for other threads to join before quitting +expert-option periodicStatsInterval --periodic-stats int :default 0 + print total time we have been running every N decisions + endmodule |