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