plus de pb avec referencemanual.sh

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8375 85f007b7-540e-0410-9357-904b9bb8a0f7

7 files changed, 30 insertions, 17 deletions

diff --git a/doc/.cvsignore b/doc/.cvsignore
index 4b0319acf..a6109f3d0 100644
--- a/doc/.cvsignore
+++ b/doc/.cvsignore
@@ -1,3 +1,4 @@
+version.tex
 *.blg
 *.ind
 *.ilg
diff --git a/doc/AddRefMan-pre.tex b/doc/AddRefMan-pre.tex
index 44af92025..d467b84e6 100644
--- a/doc/AddRefMan-pre.tex
+++ b/doc/AddRefMan-pre.tex
@@ -1,4 +1,4 @@
-\addtocontents{sh}{BEGINADDENDUM=\thepage}
+\RefManCutCommand{BEGINADDENDUM=\thepage}
 \coverpage{Addenddum to the Reference Manual}{\ }
 \addcontentsline{toc}{part}{Additional documentation}
 \setheaders{Presentation of the Addendum}
diff --git a/doc/Makefile b/doc/Makefile
index 8ab0db0e9..6f7f1fc70 100644
--- a/doc/Makefile
+++ b/doc/Makefile
@@ -288,29 +288,29 @@ Tutorial.v.pdf: ./title.tex Tutorial.v.tex
 Reference-Manual.ps: Reference-Manual.dvi
 
 Reference-Manual.dvi: $(INPUTS) $(REFMANFILES) $(COQTEXFILES) biblio.bib
-	rm -f Reference-Manual.sh
+	#rm -f Reference-Manual.sh
 	$(LATEX) Reference-Manual
-	rm Reference-Manual.sh
+	#rm Reference-Manual.sh
 	$(BIBTEX) Reference-Manual
 	$(LATEX) Reference-Manual
-	rm Reference-Manual.sh
+	#rm Reference-Manual.sh
 	$(BIBTEX) Reference-Manual
 	$(LATEX) Reference-Manual
-	rm Reference-Manual.sh
+	#rm Reference-Manual.sh
 	$(MAKEINDEX) Reference-Manual
 	$(MAKEINDEX) Reference-Manual.tacidx -o Reference-Manual.tacind
 	$(MAKEINDEX) Reference-Manual.comidx -o Reference-Manual.comind
 	$(MAKEINDEX) Reference-Manual.erridx -o Reference-Manual.errind
 	$(LATEX) Reference-Manual
-	rm Reference-Manual.sh
+	#rm Reference-Manual.sh
 	$(LATEX) Reference-Manual
 
 Reference-Manual.pdf: Reference-Manual.dvi
-	rm -f Reference-Manual.sh
+	#rm -f Reference-Manual.sh
 	$(PDFLATEX) Reference-Manual.tex
 
 quick: $(INPUTS) $(REFMANFILES) $(COQTEXFILES) biblio.bib
-	rm -f Reference-Manual.sh
+	#rm -f Reference-Manual.sh
 	$(LATEX) Reference-Manual
 
 
diff --git a/doc/RefMan-uti.tex b/doc/RefMan-uti.tex
index b812a3042..9d3f7b761 100755
--- a/doc/RefMan-uti.tex
+++ b/doc/RefMan-uti.tex
@@ -281,7 +281,7 @@ There are man pages for the commands {\tt coqdep}, {\tt gallina} and
 {\tt coq-tex}. Man pages are installed at installation time
 (see installation instructions in file {\tt INSTALL}, step 6).
 
-\addtocontents{sh}{ENDREFMAN=\thepage}
+\RefManCutCommand{ENDREFMAN=\thepage}
 
 % $Id$
 
diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex
index d4f4c4c76..493619166 100644
--- a/doc/Reference-Manual.tex
+++ b/doc/Reference-Manual.tex
@@ -67,19 +67,20 @@
 %%SUPPRIME \include{Natural.v}%
 \include{Omega.v}%
 %%SUPPRIME \include{Program.v}%
-\include{Correctness.v}% = preuve de pgms imperatifs
+%%SUPPRIME \include{Correctness.v}% = preuve de pgms imperatifs
 \include{Extraction.v}%
 \include{Polynom.v}%  = Ring
 \include{Setoid.v}% Tactique pour les setoides
-\addtocontents{sh}{ENDADDENDUM=\thepage}
+\RefManCutCommand{ENDADDENDUM=\thepage}
 
 \nocite{*}
 \bibliographystyle{plain}
 \bibliography{biblio}
-\addtocontents{sh}{psselect -q -p-$ENDREFMAN,$BEGINBIBLIO- Reference-Manual.ps Reference-Manual-base.ps}
-\addtocontents{sh}{psselect -q -p$BEGINADDENDUM-$ENDADDENDUM Reference-Manual.ps Reference-Manual-addendum.ps}
-\addtocontents{sh}{dviselect -i Reference-Manual.dvi -o Reference-Manual-base.dvi 1-$ENDREFMAN $BEGINBIBLIO-}
-\addtocontents{sh}{dviselect -i Reference-Manual.dvi -o Reference-Manual-addendum.dvi $BEGINADDENDUM-$ENDADDENDUM}
+\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
 
 \printindex
 
diff --git a/doc/Setoid.tex b/doc/Setoid.tex
index 2659cae1e..68260e085 100644
--- a/doc/Setoid.tex
+++ b/doc/Setoid.tex
@@ -157,3 +157,8 @@ The arrow tells the systems in which direction the rewriting has to be
 done. Moreover, you can use \texttt{Rewrite} for setoid
 rewriting. In that case the system will check if the term you give is
 an equality or a setoid equivalence and do the appropriate work.
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: 
diff --git a/doc/headers.tex b/doc/headers.tex
index f5b337340..cccd277c3 100644
--- a/doc/headers.tex
+++ b/doc/headers.tex
@@ -23,7 +23,7 @@
 \renewcommand{\contentsname}{%
 \protect\setheaders{Table of contents}Table of contents}
 \renewcommand{\bibname}{\protect\setheaders{Bibliography}%
-\protect\addtocontents{sh}{BEGINBIBLIO=\thepage}%
+\protect\RefManCutCommand{BEGINBIBLIO=\thepage}%
 \protect\addcontentsline{toc}{chapter}{Bibliography}Bibliography}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
@@ -45,7 +45,13 @@
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Reference-Manual.sh is generated to cut the Postscript
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
-\@starttoc{sh}
+%\@starttoc{sh}
+\newwrite\RefManCut@out%
+\immediate\openout\RefManCut@out\jobname.sh
+\newcommand{\RefManCutCommand}[1]{%
+\immediate\write\RefManCut@out{#1}}
+\newcommand{\RefManCutClose}{%
+\immediate\closeout\RefManCut@out}
 
 %%%%%%%%%%%%%%%%%%%%%%%%%%%%
 % Commands for indexes