> On 26 Aug 2016, at 3:18 AM, Richmond <richmondmathewson at gmail.com> wrote: > > It might not be a bad idea to put that into the documentation. Why? I’m in the midst of fixing it ;-)