diff options
| author | msozeau | 2009-04-08 16:41:55 +0000 |
|---|---|---|
| committer | msozeau | 2009-04-08 16:41:55 +0000 |
| commit | ffa0346f35897713b4d0638760110f7aa73a09df (patch) | |
| tree | 22d1adb8bbc9461fdf09b7ca1d966ab699380492 | |
| parent | 0cf541452e6bb56ddddfae6bd9c1e08fbd47a687 (diff) | |
Change HTML paragraph output to avoid too much space after bulleted
lists, patch by B. Pierce.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12067 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | tools/coqdoc/output.ml | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml index 0343809b02..86f3bda7e5 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 |