Done. http://bugs.python.org/issue19201
I guess I should have known that. Sorry to bother python-dev with this.
_______________________________________________ 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