why3doc: flush the output when done

parent aff6a806
......@@ -82,6 +82,7 @@ let print_file fname =
fprintf fmt "<p>%s <a href=\"index.html\">index</a></p>@\n<hr>@\n" title;
Doc_lexer.do_file fmt fname;
if not !opt_body then Doc_html.print_footer fmt ();
pp_print_flush fmt ();
close_out c
let () =
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment