From d275ce86acfa23b5f82a75ad90d1bdf630c494d8 Mon Sep 17 00:00:00 2001 From: Claudio Sacerdoti Coen Date: Mon, 4 Feb 2013 22:36:52 +0000 Subject: [PATCH] Flushing needed before closing the channel. --- matita/components/ng_extraction/ocamlExtractionTable.ml | 2 ++ 1 file changed, 2 insertions(+) diff --git a/matita/components/ng_extraction/ocamlExtractionTable.ml b/matita/components/ng_extraction/ocamlExtractionTable.ml index 148377e6f..576509a04 100644 --- a/matita/components/ng_extraction/ocamlExtractionTable.ml +++ b/matita/components/ng_extraction/ocamlExtractionTable.ml @@ -249,6 +249,8 @@ let close_file status = match ch with None -> assert false | Some ch -> + Format.pp_print_flush (snd (fst ch)) (); + Format.pp_print_flush (snd (snd ch)) (); close_out (fst (fst ch)); close_out (fst (snd ch)); let ch = None in -- 2.39.2