+ if (ErrorReport.orig_file) {
+ char *op;
+ if (ErrorReport.orig_file <= 0 || ErrorReport.orig_file > total_files)
+ op = ErrorReport.orig_source;
+ else
+ op = InputFiles[ErrorReport.orig_file-1].filename;
+ printf("(\"%s\"", op);
+ if (ErrorReport.orig_line) {
+ printf(", %d", ErrorReport.orig_line);
+ if (ErrorReport.orig_char) {
+ printf(":%d", ErrorReport.orig_char);
+ }
+ }
+ printf("): ");
+ }