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

commit d7afdb3b0fef4db30c9eb8cdad5890bfc241bb8d Merge: 4ee65a6f8 1440c2cb3 Author: George Kadianakis <desnacked@riseup.net> Date: Tue Aug 6 14:51:47 2019 +0300 Merge branch 'tor-github/pr/1195' Makefile.am | 19 +++++++++++++++--- changes/ticket31304 | 3 +++ changes/ticket31311 | 3 +++ scripts/maint/practracker/practracker_tests.py | 11 ++++++++--- scripts/maint/practracker/test_practracker.sh | 27 ++++++++++++++++---------- src/test/include.am | 6 +++++- 6 files changed, 52 insertions(+), 17 deletions(-)