force push is common procedure when pull requesting, since not all code changes are additive (some things need to be rewritten and a polluted history is no fun). Pull requests are the right time to do force pushes since you shouldn't rebase your master branch anyway. This change allows github actions to perform compilation checks after force pushes too.
force push is common procedure when pull requesting, since not all code changes are additive (some things need to be rewritten and a polluted history is no fun). Pull requests are the right time to do force pushes since you shouldn't rebase your master branch anyway. This change allows github actions to perform compilation checks after force pushes too.