Allow closing a PR with no changes #8690
Description
If a PR has no changes then it cannot be merged... but it also cannot be closed or deleted! This means it will never go away.
{{ message }}
If a PR has no changes then it cannot be merged... but it also cannot be closed or deleted! This means it will never go away.