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

[dgoulet at torproject.org]

commit 17724a7cdeb9b98539831f1164a82784f1fb050f
Merge: d3c23b079 674a821fb
Author: David Goulet <dgoulet at torproject.org>
Date:   Tue Feb 18 09:06:13 2020 -0500

    Merge branch 'tor-github/pr/1743'

 changes/ticket33192                            | 5 +++++
 contrib/client-tools/tor-resolve.py            | 2 +-
 scripts/codegen/fuzzing_include_am.py          | 2 +-
 scripts/codegen/gen_server_ciphers.py          | 2 +-
 scripts/codegen/get_mozilla_ciphers.py         | 2 +-
 scripts/codegen/makedesc.py                    | 2 +-
 scripts/maint/annotate_ifdef_directives.py     | 2 +-
 scripts/maint/checkIncludes.py                 | 2 +-
 scripts/maint/format_changelog.py              | 2 +-
 scripts/maint/lintChanges.py                   | 2 +-
 scripts/maint/locatemissingdoxygen.py          | 2 +-
 scripts/maint/practracker/includes.py          | 2 +-
 scripts/maint/practracker/metrics.py           | 2 +-
 scripts/maint/practracker/practracker.py       | 2 +-
 scripts/maint/practracker/practracker_tests.py | 2 +-
 scripts/maint/rectify_include_paths.py         | 2 +-
 scripts/maint/redox.py                         | 2 +-
 scripts/maint/sortChanges.py                   | 2 +-
 18 files changed, 22 insertions(+), 17 deletions(-)