[tor-commits] [tor/master] merge the change that 2f3ec43e5b4e wanted to merge