diff options
| author | Dmitry Vyukov <dvyukov@google.com> | 2016-02-16 15:06:24 +0100 |
|---|---|---|
| committer | Dmitry Vyukov <dvyukov@google.com> | 2016-02-16 15:06:24 +0100 |
| commit | dfa483f9860d315750ea0da2673ada6bba6fcc3c (patch) | |
| tree | c964a9dcc07851d5e4b7801ec0ecc9013238872e /executor | |
| parent | 1c8e56b1556c5a02f854cbbbbe3b34c4266f01a7 (diff) | |
manager: remove coverage info caching
The generation does not seem to take too large time.
The cache consumes memory but rarey used, so just remove it.
Makes the code much nicer.
Diffstat (limited to 'executor')
0 files changed, 0 insertions, 0 deletions