This is a follow up on the quick fix for exporting from the php-src
Github mirror[1]. Instead of hard-coding everything in the code, we
introduce a configurable `gh_url`, and use it if given. We cannot use
the repository URL, though, because the toplevel folder inside the
downloaded archive would have a different name (the shortened revision
number is expanded again); downloading from the codeload subdomain
gives the desired result.
[1] <9e1ca1002a>
Due to server overload, the snapshot downloads from http://git.php.net/
have been recently disabled. Therefore, we have to fetch the snapshots
from Github. Unfortunately, rmtools expect everything available via
GitWeb, so we can't just change the configuration in the respective INI
files, so we hack around by hard-coding the download URL. Even worse,
`wget()` apparently does not yet support redirects, so we use the
codeload subdomain directly.
For now this seems to resolve the snapshot build issues, but needs to
be properly resolved soonish.