Learn more about these different git repos.
Other Git URLs
a7f2cbc
dist-git: don't remove pr directory if the build hasn't finished yet Fixes: #2078