diff options
Diffstat (limited to 'tools/klee-replay/file-creator.c')
| -rw-r--r-- | tools/klee-replay/file-creator.c | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/tools/klee-replay/file-creator.c b/tools/klee-replay/file-creator.c index 6440b414..f6a077c2 100644 --- a/tools/klee-replay/file-creator.c +++ b/tools/klee-replay/file-creator.c @@ -478,6 +478,9 @@ int remove_callback(const char *fpath, } void replay_delete_files() { + if (keep_temps) + return; + fprintf(stderr, "KLEE-REPLAY: NOTE: removing %s\n", replay_dir); if (nftw(replay_dir, remove_callback, FOPEN_MAX, |