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