submit: better handling of divergent HEAD for pushed, but not published branches #845
Description
When submitting a branch, git-spice attempts to match the branch to open PRs on the repo in case the PR was opened without using git-spice's submit command.
Right now, this will refuse to match branches with the same name that have a different HEAD.
This has led to the following scenario for some users:
- Use git-spice to submit branch but not publish a PR.
- Create PR manually
- A CI job that updates the PR (e.g. adjusting formatting)
- Make local updates and try to submit to update the branch
The submit fails because the branch matching fails (because of divergent HEAD).
We need the following fixes here:
- when rejecting a branch because of a divergent head, prompt the user in case they know for sure that they own this branch
- submit should probably remember that it pushed this branch previously, so even if there's no PR information, it's owned by us