From 75606ec8976d524d8277b26af6ef7024fafa7089 Mon Sep 17 00:00:00 2001
From: herbelin
Date: Fri, 3 Mar 2006 16:44:29 +0000
Subject: 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
---
 doc/refman/Reference-Manual.tex | 8 --------
 1 file changed, 8 deletions(-)

(limited to 'doc')

diff --git a/doc/refman/Reference-Manual.tex b/doc/refman/Reference-Manual.tex
index 08b5275882..ddc4b46ffb 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}
 
 
-- 
cgit v1.2.3