Merge branch 'am/maint-push-doc'

* am/maint-push-doc:
Documentation: avoid using undefined parameters
Documentation: mention branches rather than heads
Documentation: remove a redundant elaboration
Documentation: git push repository can also be a remote