On Sun, Oct 7, 2018 at 7:55 AM Guido van Rossum <guido at python.org> wrote: > > OK, then maybe someone (not me) can merge https://github.com/python/peps/pull/799 for me. > Per discussion, merged. ChrisA