aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorHugo Herbelin2020-04-22 21:31:22 +0200
committerHugo Herbelin2020-04-22 21:31:22 +0200
commitad51e70a26defc2d2dbab9432eabc12b80e70838 (patch)
treedded321628dfa189957d1365a81b8f903cb35810
parent3c0ba7afdf289bc1c50f3458d6c5da685f0b160c (diff)
parent11b2ab58b5e5540bf7d0d3cd188899267766e5b6 (diff)
Merge PR #12133: coqdoc: Replace deprecated HTML attribute name with id
Reviewed-by: herbelin
-rw-r--r--tools/coqdoc/output.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/tools/coqdoc/output.ml b/tools/coqdoc/output.ml
index d6f51d7b78..def1cbbcf8 100644
--- a/tools/coqdoc/output.ml
+++ b/tools/coqdoc/output.ml
@@ -821,7 +821,7 @@ module Html = struct
| Some n -> if lev <= n then add_toc_entry (Toc_section (lev, f, r))
else ());
stop_item ();
- printf "<a name=\"%s\"></a><h%d class=\"section\">" lab lev;
+ printf "<a id=\"%s\"></a><h%d class=\"section\">" lab lev;
f ();
printf "</h%d>\n" lev
@@ -835,7 +835,7 @@ module Html = struct
let letter_index category idx (c,l) =
if l <> [] then begin
let cat = if category && idx <> "global" then "(" ^ idx ^ ")" else "" in
- printf "<a name=\"%s_%c\"></a><h2>%s %s</h2>\n" idx c (display_letter c) cat;
+ 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