r8637@thot: notin | 2006-03-14 16:00:49 +0100

 
 - intégration de doc dans le Makefile principal
 - correction d'une incompatibilité avec Tetex 3.0
 


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

1 files changed, 6 insertions, 6 deletions

diff --git a/doc/refman/RefMan-ide.tex b/doc/refman/RefMan-ide.tex
index d1497f1620..ea19f3de45 100644
--- a/doc/refman/RefMan-ide.tex
+++ b/doc/refman/RefMan-ide.tex
@@ -19,10 +19,10 @@ obviously no meaning for \CoqIDE{} being ignored.
 \begin{center}
 %HEVEA\imgsrc{coqide.png}
 %BEGIN LATEX
-\ifx\pdfoutput\undefined   % si on est pas en pdflatex
-\includegraphics[width=1.0\textwidth]{coqide.eps}
-\else
+\ifpdf   % si on est en pdflatex
 \includegraphics[width=1.0\textwidth]{coqide.png}
+\else
+\includegraphics[width=1.0\textwidth]{coqide.eps}
 \fi
 %END LATEX
 \end{center}
@@ -124,10 +124,10 @@ arguments.
 \begin{center}
 %HEVEA\imgsrc{coqide-queries.png}
 %BEGIN LATEX
-\ifx\pdfoutput\undefined   % si on est pas en pdflatex
-\includegraphics[width=1.0\textwidth]{coqide-queries.eps}
-\else
+\ifpdf  % si on est en pdflatex
 \includegraphics[width=1.0\textwidth]{coqide-queries.png}
+\else
+\includegraphics[width=1.0\textwidth]{coqide-queries.eps}
 \fi
 %END LATEX
 \end{center}