commit c3a1e15a5ec8cdb1d28e2d57a77ce5deb6da39bb Merge: 10ef7a31c 7f23d47f7 Author: teor teor@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(-)