diff options
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/cache.py | 3 | ||||
| -rw-r--r-- | tools/tempfiles.py | 3 |
2 files changed, 4 insertions, 2 deletions
diff --git a/tools/cache.py b/tools/cache.py index 78a11ba0..2958197c 100644 --- a/tools/cache.py +++ b/tools/cache.py @@ -1,4 +1,5 @@ import os.path, shutil, hashlib, cPickle +from . import tempfiles # Permanent cache for dlmalloc and stdlibc++ class Cache: @@ -14,7 +15,7 @@ class Cache: os.makedirs(self.dirname) def erase(self): - shutil.rmtree(self.dirname, ignore_errors=True) + tempfiles.try_delete(self.dirname) def get_path(self, shortname): return os.path.join(self.dirname, shortname) diff --git a/tools/tempfiles.py b/tools/tempfiles.py index 06c4d1dd..1721b2bb 100644 --- a/tools/tempfiles.py +++ b/tools/tempfiles.py @@ -6,7 +6,8 @@ def try_delete(filename): try: os.unlink(filename) except: - shutil.rmtree(filename, ignore_errors=True) + if os.path.exists(filename): + shutil.rmtree(filename, ignore_errors=True) class TempFiles: def __init__(self, tmp, save_debug_files=False): |