/* Return a copy of the filename, with an extra ".bin" at the end.
More generally, it replaces "${EXEEXT}" at the end with ".bin${EXEEXT}". */
/* Return a copy of the filename, with an extra ".bin" at the end.
More generally, it replaces "${EXEEXT}" at the end with ".bin${EXEEXT}". */