[tor-commits] [tor/release-0.4.2] Merge remote-tracking branch 'tor-github/pr/1509' into maint-0.4.2

[teor at torproject.org]

commit c3a1e15a5ec8cdb1d28e2d57a77ce5deb6da39bb
Merge: 10ef7a31c 7f23d47f7
Author: teor <teor at torproject.org>
Date:   Wed Nov 6 21:28:28 2019 +1000

    Merge remote-tracking branch 'tor-github/pr/1509' into maint-0.4.2

 changes/bug32402                   |  3 +++
 changes/bug32402_git_scripts       |  3 +++
 scripts/git/git-merge-forward.sh   |  2 +-
 scripts/git/git-pull-all.sh        |  2 +-
 scripts/git/git-push-all.sh        | 21 +++++++++++----------
 scripts/maint/checkShellScripts.sh |  6 +-----
 6 files changed, 20 insertions(+), 17 deletions(-)