On Sun, Oct 7, 2018 at 7:55 AM Guido van Rossum <gu...@python.org> wrote: > > OK, then maybe someone (not me) can merge > https://github.com/python/peps/pull/799 for me. >
Per discussion, merged. ChrisA _______________________________________________ Python-Dev mailing list Python-Dev@python.org https://mail.python.org/mailman/listinfo/python-dev Unsubscribe: https://mail.python.org/mailman/options/python-dev/archive%40mail-archive.com
