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

[nickm at torproject.org]

commit ab1f39322c22c3801ffd3a7e6842352230fff113
Merge: f6db290e5 aed82bf41
Author: Nick Mathewson <nickm at torproject.org>
Date:   Tue Jul 23 12:32:14 2019 -0400

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

 changes/bug31112                      | 3 +++
 src/core/or/circuitpadding_machines.c | 4 +---
 2 files changed, 4 insertions(+), 3 deletions(-)