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

commit 70553a91343e242e05e569d59584674a21d09679 Merge: 650bdca97 e2d3d4449 Author: George Kadianakis desnacked@riseup.net Date: Wed May 29 21:25:32 2019 +0300

Merge branch 'tor-github/pr/1037'

Makefile.am | 31 +++- changes/ticket30539 | 4 + scripts/maint/add_c_file.py | 251 +++++++++++++++++++++++++++++++++ scripts/maint/rectify_include_paths.py | 13 +- scripts/maint/updateCopyright.pl | 6 +- 5 files changed, 296 insertions(+), 9 deletions(-)