diff --git a/src/plugins/markdown-report/md_gen.ml b/src/plugins/markdown-report/md_gen.ml index cf35c41074a83e232559379ba4875d6408cf90ee..d3157522cc2207eaf88ca5de0a077b9fb0d43fbf 100644 --- a/src/plugins/markdown-report/md_gen.ml +++ b/src/plugins/markdown-report/md_gen.ml @@ -601,6 +601,11 @@ let gen_report is_draft = :: elements else elements in + let elements = + Raw "\\let\\underscore\\_" :: + Raw "\\renewcommand{\\_}{\\discretionary{\\underscore}{}{\\underscore}}" :: + elements + in let doc = { title; authors; date; elements;} in try let out = open_out (Mdr_params.Output.get()) in