From 696df507b58800a7a6b52741fd4ed859aff7b1c3 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Thu, 5 Nov 2020 16:17:37 +0100
Subject: Coqdoc: we move a newline at a better place.

This does not affect the rendering but gives better structured
html/tex files.
---
 tools/coqdoc/cpretty.mll | 2 +-
 tools/coqdoc/output.ml   | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

(limited to 'tools')

diff --git a/tools/coqdoc/cpretty.mll b/tools/coqdoc/cpretty.mll
index f2b6a3f38f..e5beab5d33 100644
--- a/tools/coqdoc/cpretty.mll
+++ b/tools/coqdoc/cpretty.mll
@@ -893,7 +893,7 @@ and doc indents = parse
        doc_bol lexbuf
       }
   | '*'* "*)" space* nl
-      { new_lines 1 lexbuf; true }
+      { new_lines 1 lexbuf; Output.char '\n'; true }
   | '*'* "*)"
       { false }
   | "$"
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index 57b2b6e620..a87dfb5b2e 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -734,7 +734,7 @@ module Html = struct
 
   let end_doc () = in_doc := false;
     stop_item ();
-    if not !raw_comments then printf "\n</div>\n"
+    if not !raw_comments then printf "</div>\n"
 
   let start_emph () = printf "<i>"
 
-- 
cgit v1.2.3