Skip to content
GitLab
Menu
Projects
Groups
Snippets
Help
Help
Support
Community forum
Keyboard shortcuts
?
Submit feedback
Contribute to GitLab
Sign in
Toggle navigation
Menu
Open sidebar
Why3
why3
Commits
47290cfa
Commit
47290cfa
authored
Oct 20, 2016
by
Jean-Christophe Filliâtre
Committed by
Guillaume Melquiond
Jan 03, 2017
Browse files
why3doc: flush the output when done
parent
0e2c6aef
Changes
1
Hide whitespace changes
Inline
Side-by-side
src/why3doc/doc_main.ml
View file @
47290cfa
...
@@ -82,6 +82,7 @@ let print_file fname =
...
@@ -82,6 +82,7 @@ let print_file fname =
fprintf
fmt
"<p>%s <a href=
\"
index.html
\"
>index</a></p>@
\n
<hr>@
\n
"
title
;
fprintf
fmt
"<p>%s <a href=
\"
index.html
\"
>index</a></p>@
\n
<hr>@
\n
"
title
;
Doc_lexer
.
do_file
fmt
fname
;
Doc_lexer
.
do_file
fmt
fname
;
if
not
!
opt_body
then
Doc_html
.
print_footer
fmt
()
;
if
not
!
opt_body
then
Doc_html
.
print_footer
fmt
()
;
pp_print_flush
fmt
()
;
close_out
c
close_out
c
let
()
=
let
()
=
...
...
Write
Preview
Supports
Markdown
0%
Try again
or
attach a new file
.
Attach a file
Cancel
You are about to add
0
people
to the discussion. Proceed with caution.
Finish editing this message first!
Cancel
Please
register
or
sign in
to comment