aboutsummaryrefslogtreecommitdiffstats
path: root/driver/Frontend.ml
diff options
context:
space:
mode:
Diffstat (limited to 'driver/Frontend.ml')
-rw-r--r--driver/Frontend.ml1
1 files changed, 1 insertions, 0 deletions
diff --git a/driver/Frontend.ml b/driver/Frontend.ml
index 5db0040f..c99da945 100644
--- a/driver/Frontend.ml
+++ b/driver/Frontend.ml
@@ -75,6 +75,7 @@ let preprocess ifile ofile =
let parse_c_file sourcename ifile =
Debug.init_compile_unit sourcename;
Sections.initialize();
+ CPragmas.reset();
(* Simplification options *)
let simplifs =
"b" (* blocks: mandatory *)