aboutsummaryrefslogtreecommitdiff
path: root/tools
diff options
context:
space:
mode:
authorLi-yao Xia2020-07-28 11:30:41 -0400
committerLi-yao Xia2020-07-28 11:30:41 -0400
commit827d430fc5645bf5ad12d0a7fc6298b56ccce5f0 (patch)
tree2a512684a8c72edc53a24a3b44e63f7cfd2ad078 /tools
parent9d8efb01fde0f9e24157872213c0595cc72efc0c (diff)
parent23303e6d2129e4e63252643fc84f42ac8dcec48c (diff)
Merge PR #12754: Fixes #12752: applying symbol escaping in coqdoc index
Reviewed-by: Lysxia
Diffstat (limited to 'tools')
-rw-r--r--tools/coqdoc/output.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index def1cbbcf8..32cf05e1eb 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -838,7 +838,7 @@ module Html = struct
printf "<a id=\"%s_%c\"></a><h2>%s %s</h2>\n" idx c (display_letter c) cat;
List.iter
(fun (id,(text,link,t)) ->
- let id' = prepare_entry id t in
+ let id' = escaped (prepare_entry id t) in
printf "<a href=\"%s\">%s</a> %s<br/>\n" link id' text) l;
printf "<br/><br/>"
end