> >>Better it get fixed in CVS. There could be more errors of this kind. > > Confused. What would you like me to do? > > Please purge the platforms directory on the server. It collides with the > PLATFORMS file on these poor pseudo-OS, that have case-insensitive > filenames. (There could also still be a directory called "hints" on the > server, it did exist some time ago. If yes please rm it too)
*POOF* -R
