diff options
| author |  letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-23 12:52:41 +0000 |
|---|---|---|
| committer | letouzey <letouzey@85f007b7-540e-0410-9357-904b9bb8a0f7> | 2012-08-23 12:52:41 +0000 |
| commit | 9f465647f3ad78e324d1c86559e8045855d1dea3 (patch) | |
| tree | bb852e5d7982f05dd55680851de9e309c0689ee7 /Makefile.doc | |
| parent | 8feaf6a1c648f78e987a9e1483816f3a5e05a179 (diff) | |
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
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 6 |
1 files changed, 2 insertions, 4 deletions
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 |