RFR: merge-bot: recreate repository on failed push

Wed Apr 8 11:37:40 UTC 2020

On Wed, 8 Apr 2020 11:24:40 GMT, Erik Helin <ehelin at openjdk.org> wrote:

> Hi all,
> 
> please review this patch that makes the merge bot recreate the repository on a
> failed push. A push can fail for a variety of reasons: network errors,
> conflicting push by another contributor, etc. The safest, and easiest, way to
> handle this scenario is to just recreate the repository. To make this operation
> cheap I made the merge bot utilize a `HostedRepositoryPool`.
> 
> Testing:
> - `make test` passes on Linux x64
> 
> Thanks,
> Erik

Looks good!

-------------

Marked as reviewed by rwestberg (Reviewer).

PR: https://git.openjdk.java.net/skara/pull/570