aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqdoc/output.ml
diff options
context:
space:
mode:
Diffstat (limited to 'tools/coqdoc/output.ml')
-rw-r--r--tools/coqdoc/output.ml6
1 files changed, 5 insertions, 1 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 0343809b0..86f3bda7e 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -554,7 +554,11 @@ module Html = struct
let end_inline_coq () = printf "</span>"
- let paragraph () = stop_item (); printf "\n<br/><br/>\n"
+ let paragraph () =
+ let i = !item_level in
+ stop_item ();
+ if i > 0 then printf "\n"
+ else printf "\n<br/> <br/>\n"
let section lev f =
let lab = new_label () in