diff options
| author | Alon Zakai <alonzakai@gmail.com> | 2013-03-05 10:13:06 -0800 |
|---|---|---|
| committer | Alon Zakai <alonzakai@gmail.com> | 2013-03-05 10:13:06 -0800 |
| commit | ce09c386442cefacad53b849347c12411c5d3930 (patch) | |
| tree | dc08f3ec7feecef5fec22b06e8c0728afa122c64 | |
| parent | c1c88e7185be8db7e38a94ceecc2a23f8cb72d7d (diff) | |
restore cache erase save times, busted by pull #826
| -rw-r--r-- | tools/cache.py | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/tools/cache.py b/tools/cache.py index d9fabf92..6647219d 100644 --- a/tools/cache.py +++ b/tools/cache.py @@ -17,6 +17,10 @@ class Cache: def erase(self): tempfiles.try_delete(self.dirname) + try: + open(Cache.dirname + '__last_clear', 'w').write('last clear: ' + time.asctime() + '\n') + except: + print >> sys.stderr, 'failed to save last clear time' def get_path(self, shortname): return os.path.join(self.dirname, shortname) |