aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/tools/coqrst/coqdomain.py2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/tools/coqrst/coqdomain.py b/doc/tools/coqrst/coqdomain.py
index 84f32e187b..0b94b0d675 100644
--- a/doc/tools/coqrst/coqdomain.py
+++ b/doc/tools/coqrst/coqdomain.py
@@ -519,7 +519,7 @@ class ProductionObject(CoqObject):
row = nodes.inline(classes=['prodn-row'])
entry = nodes.inline(classes=['prodn-cell-nonterminal'])
if lhs != "":
- target_name = 'grammar-token-' + lhs
+ target_name = 'grammar-token-' + nodes.make_id(lhs)
target = nodes.target('', '', ids=[target_name], names=[target_name])
# putting prodn-target on the target node won't appear in the tex file
inline = nodes.inline(classes=['prodn-target'])