We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Currently GitHub returns an error when Pull tries to merge into a protected branch. The PR will just stay open ready to be manually merged.
An improvement will be commenting on the PR when this happens.