diff options
| author | Dmitry Vyukov <dvyukov@google.com> | 2016-02-16 17:04:38 +0100 |
|---|---|---|
| committer | Dmitry Vyukov <dvyukov@google.com> | 2016-02-18 21:41:50 +0100 |
| commit | 8e0d5c2bd01651bfa775f3cf3df9823e8a8faa31 (patch) | |
| tree | f85b2b3d7ee058dedcc719c824798ed82e6a5fc0 /executor | |
| parent | 96949534aed13633c1ad9f015a6c7055cb30649c (diff) | |
manager: properly cleanup on ctrl+C
Don't leave temporal files behind.
Diffstat (limited to 'executor')
0 files changed, 0 insertions, 0 deletions