diff options
Diffstat (limited to 'Doc/lib')
| -rw-r--r-- | Doc/lib/libdoctest.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Doc/lib/libdoctest.tex b/Doc/lib/libdoctest.tex index 314cdb3..c0bdf6d 100644 --- a/Doc/lib/libdoctest.tex +++ b/Doc/lib/libdoctest.tex @@ -362,7 +362,7 @@ example: \begin{productionlist}[doctest] \production{directive} - {"#" "doctest:" \token{on_or_off} \token{directive_name}} + {"\#" "doctest:" \token{on_or_off} \token{directive_name}} \production{on_or_off} {"+" | "-"} \production{directive_name} |