diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml index ed6f85bd85691f5dd18ccd5f39f574a501d890f8..12322e06cb3f7824cee858fed6f8a5cb0f7f71e7 100644 --- a/src/plugins/markdown-report/md_gen.ml +++ b/src/plugins/markdown-report/md_gen.ml @@ -102,12 +102,15 @@ let section_stubs env = let kf = Globals.Functions.find_by_name s in let content = if env.is_draft then insert_marks - else - [ Block - [ Text - [Inline_code s; Plain "has the following specification"]; - codelines - "acsl" Printer.pp_funspec (Annotations.funspec kf)]] + else begin + let comment = insert_remark env s in + Block + [ Text + [Inline_code s; Plain "has the following specification"]; + codelines + "acsl" Printer.pp_funspec (Annotations.funspec kf)] + :: comment + end in H4 ([Inline_code s], Some s) :: content) l