Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
doc: Document forced pushing with git
Mention that we generally disallow forced pushes but allow it in trivial cases within 10 minutes of the original push unless the branch pushed to already has new commits. PR-URL: #1420 Reviewed-By: Rod Vagg <[email protected]> Reviewed-By: Jeremiah Senkpiel <[email protected]> Reviewed-By: Roman Reiss <[email protected]>
- Loading branch information