Avi Kivity 4456645f97 scripts: pull_pr.sh: auto-close pull request after merge ...

Add a "Closes #$PR_NUM" annotation at the end of the commit
message to tell github to close the pull request, preventing
manual work and/or dangling pull requests.

Closes #7245

2020-09-16 10:23:34 +02:00

1.4 KiB

Executable File

Raw Blame History

View Raw