diff options
Diffstat (limited to 'doc/Reference-Manual.tex')
| -rw-r--r-- | doc/Reference-Manual.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex index 516a3f9d9..1d324b786 100644 --- a/doc/Reference-Manual.tex +++ b/doc/Reference-Manual.tex @@ -7,7 +7,7 @@ \makeatletter -%\includeonly{Polynom.v} +%\includeonly{RefMan-syn.v} \input{./macros.tex}% extension .tex pour htmlgen \input{./title.tex}% extension .tex pour htmlgen |