| commit | c89061817b4364dd5df4e67e1b3aa8a7bc60c997 | [log] [tgz] |
|---|---|---|
| author | Johannes Gijsbers <jlg@dds.nl> | Fri Aug 20 14:37:05 2004 +0000 |
| committer | Johannes Gijsbers <jlg@dds.nl> | Fri Aug 20 14:37:05 2004 +0000 |
| tree | 9297f84235421699725fb50a28dc0467c80ddd41 | |
| parent | 37af986ebf7e43be683e2539ba918251f5fc7d21 [diff] |
Quote # as \# to make lib compile again.
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 @@ \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}