[tor-commits] [tor/master] Merge branch 'tor-github/pr/800' into maint-0.4.0

commit 747b74c1825de055bd027c9c74088efdd61d7481 Merge: d016bbaa7 d194f6bed Author: George Kadianakis desnacked@riseup.net Date: Fri Apr 5 14:51:21 2019 +0300

Merge branch 'tor-github/pr/800' into maint-0.4.0

changes/ticket29357 | 7 +++++++ doc/tor.1.txt | 15 +++++++++++++++ src/app/config/config.c | 1 + src/app/config/or_options_st.h | 5 +++++ src/core/mainloop/netstatus.c | 4 ++++ src/test/test_mainloop.c | 8 ++++++++ 6 files changed, 40 insertions(+)