From 4304b761542a31324c5327acee40cd737f75f61c Mon Sep 17 00:00:00 2001 From: Alasdair Date: Thu, 25 Apr 2024 22:52:39 +0100 Subject: [PATCH] Handle empty lines after * prefix in doc comments --- src/lib/lexer.mll | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/lib/lexer.mll b/src/lib/lexer.mll index cecb9e2aa..ab890f25a 100644 --- a/src/lib/lexer.mll +++ b/src/lib/lexer.mll @@ -297,6 +297,12 @@ and doc_comment pos b depth lstart = parse doc_comment pos b (depth - 1) false lexbuf ) } | "\n" { Buffer.add_string b "\n"; Lexing.new_line lexbuf; doc_comment pos b depth true lexbuf } + | wsc+ "*\n" as prefix { if lstart then ( + Buffer.add_string b "\n"; + doc_comment pos b depth true lexbuf + ) else ( + Buffer.add_string b prefix; doc_comment pos b depth true lexbuf + ) } | wsc+ "*" wsc as prefix { if lstart then ( Buffer.add_string b (String.make (String.length prefix - 3) ' '); doc_comment pos b depth false lexbuf