Doing an "ours" merge to avoid taking 35699ef9f5d2814203653e16c, which is a cherry-picked backport of 9686.
Nick Mathewson