Thanks for the reminder -- had forgotten about that. I'll open a separate issue for changing the name of this file.