diff options
| author | Alon Zakai <alonzakai@gmail.com> | 2013-02-26 13:51:42 -0500 |
|---|---|---|
| committer | Alon Zakai <alonzakai@gmail.com> | 2013-02-26 13:51:42 -0500 |
| commit | 556bb55f1b79f5b1420d5cf6d124631aea247a43 (patch) | |
| tree | 4b55361c84508d71441b13b84ff237dfe2218cf1 /tools/shared.py | |
| parent | 54f71a8237cba633dba6bd12bd5167987a814792 (diff) | |
save last cache clear time
Diffstat (limited to 'tools/shared.py')
| -rw-r--r-- | tools/shared.py | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/tools/shared.py b/tools/shared.py index 869ac1b6..1f1016cd 100644 --- a/tools/shared.py +++ b/tools/shared.py @@ -1174,6 +1174,10 @@ class Cache: except: pass try_delete(RELOOPER) + try: + open(Cache.dirname + '__last_clear', 'w').write('last clear: ' + time.asctime() + '\n') + except: + print >> sys.stderr, 'failed to save last clear time' # Request a cached file. If it isn't in the cache, it will be created with # the given creator function |