[tor-commits] [tor/maint-0.4.0] 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(+)