--- output.c.orig	2016-06-03 14:35:09.000000000 -0500
+++ output.c	2016-08-28 12:35:51.000000000 -0500
@@ -271,6 +271,7 @@
 void
 output_line (FILE *f, int line_number, const char *file_name)
 {
+  if (line_flag) return;
   output_string (f, "\n#line ");
   output_decimal_number (f, line_number, 0);
   output_string (f, " \"");
@@ -281,6 +282,7 @@
 void
 output_current_line (FILE *f)
 {
+  if (line_flag) return;
   output_string (f, "\n#line ");
   if (f == output_interface_file)
     {