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

[nickm at torproject.org]

commit ee6f54ff3f508ff7d0e169150ebc8519752d69ad
Merge: b547ece92 a10d4adc2
Author: Nick Mathewson <nickm at torproject.org>
Date:   Wed Apr 3 08:33:40 2019 -0400

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

 changes/ticket29913                      | 4 ++++
 scripts/maint/checkIncludes.py           | 2 +-
 scripts/maint/practracker/practracker.py | 2 +-
 scripts/maint/rectify_include_paths.py   | 2 +-
 src/config/mmdb-convert.py               | 2 +-
 src/test/ope_ref.py                      | 2 +-
 6 files changed, 9 insertions(+), 5 deletions(-)