[tor-commits] [tor/master] Merge branch 'tor-github/pr/1312'

commit 987742373645d4d4de20059066ef1855478753e7 Merge: 8377b610b f0044e44f Author: George Kadianakis desnacked@riseup.net Date: Mon Sep 16 19:44:33 2019 +0300

Merge branch 'tor-github/pr/1312'

changes/ticket31678 | 4 ++ scripts/git/git-merge-forward.sh | 63 ++++++++++++++-------- scripts/git/git-pull-all.sh | 92 ++++++++++++++++++++++---------- scripts/git/git-push-all.sh | 111 +++++++++++++++++++++++++++++---------- 4 files changed, 194 insertions(+), 76 deletions(-)