diff options
| author | Dmitry Vyukov <dvyukov@google.com> | 2024-07-01 14:26:05 +0200 |
|---|---|---|
| committer | Dmitry Vyukov <dvyukov@google.com> | 2024-07-02 08:23:18 +0000 |
| commit | 9e5bd0be6b4daaf4593959c6c1a3708cfc1d0969 (patch) | |
| tree | 124f1de3d139a28490fc933676718ad8c0ef1f8d /executor | |
| parent | b01b098ace00ac799e10c38d3d3f1db50437eb57 (diff) | |
pkg/mgrconfig: allow to disable remote coverage and coverage edges
Diffstat (limited to 'executor')
| -rw-r--r-- | executor/executor.cc | 16 |
1 files changed, 9 insertions, 7 deletions
diff --git a/executor/executor.cc b/executor/executor.cc index fb5d242de..862b0776e 100644 --- a/executor/executor.cc +++ b/executor/executor.cc @@ -990,13 +990,15 @@ void execute_one() #endif write_extra_output(); - // Check for new extra coverage in small intervals to avoid situation - // that we were killed on timeout before we write any. - // Check for extra coverage is very cheap, effectively a memory load. - const uint64 kSleepMs = 100; - for (uint64 i = 0; i < prog_extra_cover_timeout / kSleepMs; i++) { - sleep_ms(kSleepMs); - write_extra_output(); + if (flag_extra_coverage) { + // Check for new extra coverage in small intervals to avoid situation + // that we were killed on timeout before we write any. + // Check for extra coverage is very cheap, effectively a memory load. + const uint64 kSleepMs = 100; + for (uint64 i = 0; i < prog_extra_cover_timeout / kSleepMs; i++) { + sleep_ms(kSleepMs); + write_extra_output(); + } } } |
