Don't update the database during redo-ood.
Makes it slightly faster.
This commit is contained in:
parent
3b19ccad9f
commit
560f95fd77
3 changed files with 23 additions and 6 deletions
13
redo-ood.py
13
redo-ood.py
|
|
@ -11,7 +11,18 @@ if len(sys.argv[1:]) != 0:
|
|||
err('%s: no arguments expected.\n' % sys.argv[0])
|
||||
sys.exit(1)
|
||||
|
||||
|
||||
cache = {}
|
||||
|
||||
def is_checked(f):
|
||||
return cache.get(f.id, 0)
|
||||
|
||||
def set_checked(f):
|
||||
cache[f.id] = 1
|
||||
|
||||
|
||||
for f in state.files():
|
||||
if f.is_generated and f.read_stamp() != state.STAMP_MISSING:
|
||||
if deps.isdirty(f, depth='', max_changed=vars.RUNID):
|
||||
if deps.isdirty(f, depth='', max_changed=vars.RUNID,
|
||||
is_checked=is_checked, set_checked=set_checked):
|
||||
print f.nicename()
|
||||
|
|
|
|||
Loading…
Add table
Add a link
Reference in a new issue