diff options
| author | letouzey | 2012-08-23 12:52:41 +0000 |
|---|---|---|
| committer | letouzey | 2012-08-23 12:52:41 +0000 |
| commit | 9f465647f3ad78e324d1c86559e8045855d1dea3 (patch) | |
| tree | bb852e5d7982f05dd55680851de9e309c0689ee7 /Makefile.common | |
| 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.common')
| -rw-r--r-- | Makefile.common | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/Makefile.common b/Makefile.common index 4f0aa4195f..7925474bac 100644 --- a/Makefile.common +++ b/Makefile.common @@ -114,8 +114,8 @@ HEVEA:=hevea HEVEAOPTS:=-fix -exec xxdate.exe HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea HTMLSTYLE:=simple -export TEXINPUTS:=$(COQSRC)/doc:$(HEVEALIB): -COQTEXOPTS:=-n 72 -image "$(COQSRC)/$(COQTOPEXE) -boot" -sl -small +export TEXINPUTS:=$(HEVEALIB): +COQTEXOPTS:=-n 72 -image "$(COQTOPEXE) -boot" -sl -small DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex |