Re: [wwwdocs] Recommend reviewing local changes before pushing them

2020-01-14 Thread Jonathan Wakely
On 14/01/20 16:00 +0100, Andreas Schwab wrote: On Jan 14 2020, Jonathan Wakely wrote: You can also just do "git log" and check which commits are more recent than the one shown as the upstream: $ git log commit 9e502f6deae9f821bd7079aad5f98a4f3bae15cf (HEAD -> master) Author: Jonathan Wakely D

Re: [wwwdocs] Recommend reviewing local changes before pushing them

2020-01-14 Thread Andreas Schwab
On Jan 14 2020, Jonathan Wakely wrote: > You can also just do "git log" and check which commits are more recent > than the one shown as the upstream: > > $ git log > commit 9e502f6deae9f821bd7079aad5f98a4f3bae15cf (HEAD -> master) > Author: Jonathan Wakely > Date: Tue Jan 14 13:34:02 2020 +

Re: [wwwdocs] Recommend reviewing local changes before pushing them

2020-01-14 Thread Richard Biener
On Tue, Jan 14, 2020 at 3:28 PM Jonathan Wakely wrote: > > On 14/01/20 15:08 +0100, Richard Biener wrote: > >On Tue, Jan 14, 2020 at 2:37 PM Jonathan Wakely wrote: > >> > >> I really think people should be reviewing what they're about to push > >> before doing it. > >> > >> OK for wwwdocs? > > >

Re: [wwwdocs] Recommend reviewing local changes before pushing them

2020-01-14 Thread Jonathan Wakely
On 14/01/20 13:39 +, Richard Earnshaw wrote: On 14/01/2020 13:37, Jonathan Wakely wrote: I really think people should be reviewing what they're about to push before doing it. OK for wwwdocs? I'd recommend git push origin HEAD: rather than just 'git push' Otherwise, OK. Here's a diff

Re: [wwwdocs] Recommend reviewing local changes before pushing them

2020-01-14 Thread Jonathan Wakely
On 14/01/20 15:08 +0100, Richard Biener wrote: On Tue, Jan 14, 2020 at 2:37 PM Jonathan Wakely wrote: I really think people should be reviewing what they're about to push before doing it. OK for wwwdocs? So I figure that first doing the git push with -n -v and then reviewing the pushed chan

Re: [wwwdocs] Recommend reviewing local changes before pushing them

2020-01-14 Thread Richard Biener
On Tue, Jan 14, 2020 at 2:37 PM Jonathan Wakely wrote: > > I really think people should be reviewing what they're about to push > before doing it. > > OK for wwwdocs? So I figure that first doing the git push with -n -v and then reviewing the pushed changes (cut&paste the revision range) with git

Re: [wwwdocs] Recommend reviewing local changes before pushing them

2020-01-14 Thread Richard Earnshaw
On 14/01/2020 13:37, Jonathan Wakely wrote: > I really think people should be reviewing what they're about to push > before doing it. > > OK for wwwdocs? > I'd recommend git push origin HEAD: rather than just 'git push' Otherwise, OK. R.

[wwwdocs] Recommend reviewing local changes before pushing them

2020-01-14 Thread Jonathan Wakely
I really think people should be reviewing what they're about to push before doing it. OK for wwwdocs? commit 2c54cb9e98fe67096b62718d8dbd3b2ca485ff89 Author: Jonathan Wakely Date: Tue Jan 14 13:34:02 2020 + Recommend reviewing local changes before pushing them diff --git a/htdocs/git