/* File name specified with -o for the output file, or 0 if no -o. */
extern char *spec_outfile;
/* File name for the parser (i.e., the one above, or its default.) */
extern char *parser_file_name;
/* File name specified with -o for the output file, or 0 if no -o. */
extern char *spec_outfile;
/* File name for the parser (i.e., the one above, or its default.) */
extern char *parser_file_name;