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

[nickm at torproject.org]

commit 409e1ca3d59be8530d8299215841410cf2f344ba
Merge: 9f7e1ccac dfa1800c7
Author: Nick Mathewson <nickm at 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(-)