diff options
| author |  herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-03 16:44:29 +0000 |
|---|---|---|
| committer | herbelin <herbelin@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2006-03-03 16:44:29 +0000 |
| commit | 75606ec8976d524d8277b26af6ef7024fafa7089 (patch) | |
| tree | f6a94528a0af5d2baa902b00fdfd41bbfd2b4408 | |
| parent | 40cd2418ddaf543c02426ca8bdd2bc2ebc4cba01 (diff) | |
Suppression de la coupure entre base et addendum (quitte à le remettre si demandes)
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8613 85f007b7-540e-0410-9357-904b9bb8a0f7
| -rw-r--r-- | doc/refman/Reference-Manual.tex | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex index 08b527588..ddc4b46ff 100644 --- a/doc/refman/Reference-Manual.tex +++ b/doc/refman/Reference-Manual.tex @@ -115,14 +115,6 @@ \addcontentsline{toc}{chapter}{\listfigurename} %END LATEX -%BEGIN LATEX -\RefManCutCommand{psselect -q -p-$ENDREFMAN,$BEGINBIBLIO- Reference-Manual.ps Reference-Manual-base.ps} -\RefManCutCommand{psselect -q -p$BEGINADDENDUM-$ENDADDENDUM Reference-Manual.ps Reference-Manual-addendum.ps} -\RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-base.dvi 1-$ENDREFMAN $BEGINBIBLIO-} -\RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-addendum.dvi $BEGINADDENDUM-$ENDADDENDUM} -\RefManCutClose -%END LATEX - \end{document} |