[tor-commits] [tor/master] Merge remote-tracking branch 'tor-github/pr/1272'

[nickm at torproject.org]

commit 78307ed1866ffdec58aaac14f24ba3d77c571f59
Merge: 01bda9bed e155598fe
Author: Nick Mathewson <nickm at torproject.org>
Date:   Mon Sep 2 14:13:32 2019 -0400

    Merge remote-tracking branch 'tor-github/pr/1272'

 changes/ticket31314              |  18 +++
 scripts/git/git-merge-forward.sh | 281 +++++++++++++++++++++++++++++++--------
 scripts/git/git-push-all.sh      | 219 +++++++++++++++++++++++++++---
 3 files changed, 445 insertions(+), 73 deletions(-)