Learn more about these different git repos.
Other Git URLs
No commits found
Fixes: #942
This change takes approach #2 from the above issue. We keep a record of recently completed repo tasks to avoid duplicate regens in a race.
@julian8628 please review
could we make this timeout configurable?
I wasn't planning on it, but I guess it couldn't hurt to make it tuneable.
1 new commit added
make recent_tasks lifetime configurable
Commit 2b8a9dd fixes this pull-request
Pull-Request has been merged by mikem
Fixes: #942
This change takes approach #2 from the above issue. We keep a record of recently completed repo tasks to avoid duplicate regens in a race.