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

[asn at torproject.org]

commit 7157d80c6f0dc2bdcaf8993f5010f0e8d791c675
Merge: 01a797be4 82ad63ef4
Author: George Kadianakis <desnacked at riseup.net>
Date:   Wed Sep 25 14:19:49 2019 +0300

    Merge branch 'tor-github/pr/1337'

 Makefile.am                                                   | 1 +
 changes/ticket31338                                           | 4 ++++
 scripts/maint/practracker/practracker.py                      | 9 +++++++++
 scripts/maint/practracker/problem.py                          | 6 ++++--
 scripts/maint/practracker/test_practracker.sh                 | 6 ++++++
 scripts/maint/practracker/testdata/ex1-overbroad-expected.txt | 2 ++
 scripts/maint/practracker/testdata/ex1.txt                    | 5 ++++-
 scripts/maint/practracker/util.py                             | 7 +++++++
 8 files changed, 37 insertions(+), 3 deletions(-)