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

[teor at torproject.org]

commit 697527764921d95f2ef03f0c0418e2c0e88f5187
Merge: 4f88eb849 5ad1efa06
Author: teor <teor at torproject.org>
Date:   Mon Jan 20 15:40:08 2020 +1000

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

 scripts/maint/add_c_file.py | 200 +++++++++++++++++++++++++++++++-------------
 1 file changed, 141 insertions(+), 59 deletions(-)