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

commit 125a6300da5412ce5fb2c0506f699e653a7ea6dc Merge: 93ca08d66 66a15013f Author: Nick Mathewson <nickm@torproject.org> Date: Tue Jun 18 09:10:34 2019 -0400 Merge remote-tracking branch 'tor-github/pr/1115' changes/ticket19381 | 4 ++++ configure.ac | 8 ++++++++ doc/include.am | 23 +++++++++++++++++++---- 3 files changed, 31 insertions(+), 4 deletions(-)