From 50223653a4568c124f36db0d91122fc69c9642cd Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?C=C3=A9dric=20Pasteur?= <cedric.pasteur@ens.fr>
Date: Mon, 13 Sep 2010 15:15:13 +0200
Subject: [PATCH] Do not forget to flush the output

The end of some header files was not printed.
---
 compiler/obc/c/c.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/compiler/obc/c/c.ml b/compiler/obc/c/c.ml
index 1f2a5a8..da14cf1 100644
--- a/compiler/obc/c/c.ml
+++ b/compiler/obc/c/c.ml
@@ -287,7 +287,7 @@ let pp_cfile_desc fmt filen cfile =
         iter (fun d -> fprintf fmt "#include \"%s.h\"@\n" d)
           deps;
         iter (pp_cdecl fmt) cdecls;
-        fprintf fmt "#endif // %s_H@\n" headern_macro
+        fprintf fmt "#endif // %s_H@\n@?" headern_macro
     | Csource cdefs ->
         let headern = filen_wo_ext ^ ".h" in
         Misc.print_header_info fmt "/*" "*/";