Quote # as \# to make lib compile again.

diff --git a/Doc/lib/libdoctest.tex b/Doc/lib/libdoctest.tex
index 314cdb372afe36c0913f8ce146859afe21f4f758..c0bdf6de66838d0d986148e307cd5680b6ef5c2a 100644 (file)
--- 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}