From 0bda4944e866556a6347bdc74ff1b099e61add4d Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Wed, 29 Nov 2017 19:11:01 +0100 Subject: [PATCH] Escape unrecognized identifiers as they may contain '<' or '>'. --- src/why3doc/doc_lexer.mll | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/why3doc/doc_lexer.mll b/src/why3doc/doc_lexer.mll index 0a5519f5e..f6e4d59b9 100644 --- a/src/why3doc/doc_lexer.mll +++ b/src/why3doc/doc_lexer.mll @@ -74,7 +74,7 @@ Doc_def.pp_locate id Pp.html_string s with Not_found -> (* otherwise, just print it *) - pp_print_string fmt s + Pp.html_string fmt s end type empty_line = PrevEmpty | CurrEmpty | NotEmpty -- GitLab