aboutsummaryrefslogtreecommitdiffstats
path: root/exportclight/Clightgen.ml
diff options
context:
space:
mode:
authorXavier Leroy <xavier.leroy@inria.fr>2015-04-23 11:56:13 +0200
committerXavier Leroy <xavier.leroy@inria.fr>2015-04-23 11:56:13 +0200
commit8c2e9c25bab0118a71fe27bbe539ac6464effde2 (patch)
treee32f30b96f89192293a62696cf6434a94b0bc981 /exportclight/Clightgen.ml
parent0bf99217426a44046ef0aaa7f84a9b2a3646ed89 (diff)
downloadcompcert-8c2e9c25bab0118a71fe27bbe539ac6464effde2.tar.gz
compcert-8c2e9c25bab0118a71fe27bbe539ac6464effde2.zip
Update clightgen to the new annotations and the new inline asm.
Diffstat (limited to 'exportclight/Clightgen.ml')
-rw-r--r--exportclight/Clightgen.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/exportclight/Clightgen.ml b/exportclight/Clightgen.ml
index c1009b4f..a1dba2d9 100644
--- a/exportclight/Clightgen.ml
+++ b/exportclight/Clightgen.ml
@@ -112,7 +112,7 @@ let parse_c_file sourcename ifile =
in
(* Parsing and production of a simplified C AST *)
let ast =
- match Parse.preprocessed_file simplifs sourcename ifile with
+ match fst (Parse.preprocessed_file simplifs sourcename ifile) with
| None -> exit 2
| Some p -> p in
(* Save C AST if requested *)