On Sun, Oct 7, 2018 at 7:55 AM Guido van Rossum <[email protected]> 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 [email protected] https://mail.python.org/mailman/listinfo/python-dev Unsubscribe: https://mail.python.org/mailman/options/python-dev/archive%40mail-archive.com
