diff options
Diffstat (limited to 'doc/tools/coqrst/notations/plain.py')
| -rw-r--r-- | doc/tools/coqrst/notations/plain.py | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/tools/coqrst/notations/plain.py b/doc/tools/coqrst/notations/plain.py index 93a7ec4683..23996b0d63 100644 --- a/doc/tools/coqrst/notations/plain.py +++ b/doc/tools/coqrst/notations/plain.py @@ -53,7 +53,7 @@ class TacticNotationsToDotsVisitor(TacticNotationsVisitor): self.buffer.write("‘{}’".format(ctx.ID().getText()[1:])) def visitEscaped(self, ctx:TacticNotationsParser.EscapedContext): - self.buffer.write(ctx.ESCAPED().getText()[1:]) + self.buffer.write(ctx.ESCAPED().getText().replace("%", "")) def visitWhitespace(self, ctx:TacticNotationsParser.WhitespaceContext): self.buffer.write(" ") |