aboutsummaryrefslogtreecommitdiffstats
path: root/export/ExportClight.ml
diff options
context:
space:
mode:
Diffstat (limited to 'export/ExportClight.ml')
-rw-r--r--export/ExportClight.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/export/ExportClight.ml b/export/ExportClight.ml
index 421db5ed..e3b00986 100644
--- a/export/ExportClight.ml
+++ b/export/ExportClight.ml
@@ -233,7 +233,7 @@ let print_program p prog sourcefile normalized =
name_program prog;
fprintf p "@[<v 0>";
fprintf p "%s" prologue;
- print_clightgen_info ~sourcefile ~normalized p;
+ print_gen_info ~sourcefile ~normalized p;
define_idents p;
List.iter (print_globdef p) prog.Ctypes.prog_defs;
fprintf p "Definition composites : list composite_definition :=@ ";