diff --git a/Doc/lib/libdoctest.tex b/Doc/lib/libdoctest.tex
index 314cdb372af..c0bdf6de668 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}