Update 'git push' command in GettingStarted guide
authorDiego Caballero <diego.caballero@intel.com>
Tue, 2 Jun 2020 17:14:17 +0000 (20:14 +0300)
committerDiego Caballero <diego.caballero@intel.com>
Tue, 2 Jun 2020 18:25:29 +0000 (21:25 +0300)
commitb78b98491adad1390c23a78a1d207d965d5c88f3
tree64a3b4682e53f4c507963287339a8013c643bd44
parent7096e04a6831d4668c39b388ccd166f84de69191
Update 'git push' command in GettingStarted guide

'git push' command, without any other arguments, can do different
things depending on the local configuration of Git. This patch
updates the 'git push' command with extra arguments to be more
resilient to any local configuration.

Reviewed By: mehdi_amini

Differential Revision: https://reviews.llvm.org/D79964
llvm/docs/Phabricator.rst