Avi Kivity 719724e4df scripts: pull_github_pr.sh: support recovering from a failed cherry-pick ...

If a single-patch pull request fails cherry-picking, it's still possible
to recover it (if it's a simple conflict). Give the maintainer the option
by opening a subshell and instructing them to either complete the cherry-pick
or abort it.

Closes #10949

2022-07-04 09:26:45 +03:00

2.8 KiB

Executable File

Raw Blame History

View Raw