[tor-commits] [tor/release-0.4.3] Merge remote-tracking branch 'tor-github/pr/1716/head' into maint-0.4.3

commit 409e1ca3d59be8530d8299215841410cf2f344ba Merge: 9f7e1ccac dfa1800c7 Author: Nick Mathewson <nickm@torproject.org> Date: Tue Feb 11 08:44:18 2020 -0500 Merge remote-tracking branch 'tor-github/pr/1716/head' into maint-0.4.3 .gitlab-ci.yml | 30 ------------------------------ changes/ticket33213 | 3 +++ 2 files changed, 3 insertions(+), 30 deletions(-)