/* 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;