bug in src/file-coding.h