diff options
| author | Enrico Tassi | 2016-05-31 14:42:49 +0200 |
|---|---|---|
| committer | Enrico Tassi | 2016-05-31 14:42:49 +0200 |
| commit | d46e4bc63587c1b628cc80b3eac7a132a58d534d (patch) | |
| tree | 00ae2ded7013e15fcf5c98223fe20e64e0fd6454 /kernel/nativecode.ml | |
| parent | b3485ddc8c4f98743426bb58c8d49b76edd43d61 (diff) | |
STM delegation policy can be customized
The command line option is named:
- async-proofs-delegation-threshold
Values are of type float, default 1.0 (seconds).
Proofs taking less that the threshold are not delegated to
a worker.
Diffstat (limited to 'kernel/nativecode.ml')
0 files changed, 0 insertions, 0 deletions