#415 Retry when fetching files from dist-git
Merged by jkaluza. Opened by yashn.
retry_git_operation  into  master

Download 415.patch
no initial comment

Commit 194edef8 fixes this pull-request

Pull-Request has been merged by jkaluza

Pull-Request has been merged by jkaluza

Metadata