From 9f465647f3ad78e324d1c86559e8045855d1dea3 Mon Sep 17 00:00:00 2001
From: letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 23 Aug 2012 12:52:41 +0000
Subject: configure: get rid of the -src option and of ${COQSRC}

 The -src option was antic and probably broken (many references
 to source files without the $COQRSC prefix). Instead, it's quite
 simpler to refer to paths in relative way (and safer in win32
 where the base path may include spaces and other horrors).

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15748 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 Makefile.doc | 6 ++----
 1 file changed, 2 insertions(+), 4 deletions(-)

(limited to 'Makefile.doc')

diff --git a/Makefile.doc b/Makefile.doc
index ab5e193f2..220197445 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -1,7 +1,5 @@
 # Makefile for the Coq documentation
 
-# COQSRC needs to be set to a coq source repository
-
 # To compile documentation, you need the following tools:
 # Dvi: latex (latex2e), bibtex, makeindex
 # Pdf: pdflatex
@@ -53,10 +51,10 @@ rectutorial: doc/RecTutorial/RecTutorial.html \
 
 ifdef QUICK
 %.v.tex: %.tex
-	(cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`)
+	$(COQTEX) $(COQTEXOPTS) $<
 else
 %.v.tex: %.tex $(COQTEX) $(COQTOPEXE) $(PLUGINSVO) $(THEORIESVO)
-	(cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`)
+	$(COQTEX) $(COQTEXOPTS) $<
 endif
 
 %.ps: %.dvi
-- 
cgit v1.2.3