[Python-Dev] Re: What is __int__ still useful for?