diff options
Diffstat (limited to 'executor/executor.cc')
| -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(); + } } } |