/* Append to FILENAME the extension EXT, unless the result would be too long,
in which case just append the character E. */
void
/* Append to FILENAME the extension EXT, unless the result would be too long,
in which case just append the character E. */
void