diff options
author | Tobias Klauser <tklauser@distanz.ch> | 2017-01-12 10:49:32 +0100 |
---|---|---|
committer | Will Estes <westes575@gmail.com> | 2017-01-12 17:44:00 -0500 |
commit | de0c5e91df965b014b0c0a6f27cafd30a65a7065 (patch) | |
tree | 5087f83ca3e84f9d16fa7f568b1c3223d11cf3bd /src | |
parent | 84a9a4b9fca2717f23729101449a5fdae9ba9b60 (diff) |
filter: Don't emit #line if %option noline set
One place emitting a #line directive to the generated header was
missed in commit 647a92b9f4 when resolving #55. Fix it to respect
gen_line_dirs as well.
Diffstat (limited to 'src')
-rw-r--r-- | src/filter.c | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/filter.c b/src/filter.c index 9d0ace5..33e5ced 100644 --- a/src/filter.c +++ b/src/filter.c @@ -296,7 +296,8 @@ int filter_tee_header (struct filter *chain) fprintf (to_h, "\n"); /* write a fake line number. It will get fixed by the linedir filter. */ - fprintf (to_h, "#line 4000 \"M4_YY_OUTFILE_NAME\"\n"); + if (gen_line_dirs) + fprintf (to_h, "#line 4000 \"M4_YY_OUTFILE_NAME\"\n"); fprintf (to_h, "#undef %sIN_HEADER\n", prefix); fprintf (to_h, "#endif /* %sHEADER_H */\n", prefix); |