fprintf(header_file, "#define TRVSIZ 885\n");
fprintf(header_file, "#define TOKLEN %d\n", TOKLEN);
fprintf(header_file, "#define HINTLEN %d\n", HINTLEN);
fprintf(header_file, "#define TRVSIZ 885\n");
fprintf(header_file, "#define TOKLEN %d\n", TOKLEN);
fprintf(header_file, "#define HINTLEN %d\n", HINTLEN);