Possible race when pushing quickly several times to a PR

[Zimmi48]

People can push quickly several times to a PR, especially when using GitHub's suggestion feature, and applying suggestions. If the make-ancestor.sh script is run several times in parallel for the same PR, the script can fail with:

fatal: 'pr-10002' is already checked out at '/tmp/tmp.oKe1DcAZKW'

leading to a wrong conclusion that the current PR cannot be merged with the base branch.

Another race that can also happen in this case is a rebase label being set with a delay. Meanwhile the next push has produced a successful merge which should lead to removing the rebase label if it is set. But it isn't the case yet.