diff options
| author |  Stephane Glondu <steph@glondu.net> | 2012-12-29 10:57:43 +0100 |
|---|---|---|
| committer | Stephane Glondu <steph@glondu.net> | 2012-12-29 10:57:43 +0100 |
| commit | bf12eb93f3f6a6a824a10878878fadd59745aae0 (patch) | |
| tree | 279f64f4b7e4804415ab5731cc7aaa8a4fcfe074 /Makefile.common | |
| parent | e0d682ec25282a348d35c5b169abafec48555690 (diff) | |
Imported Upstream version 8.4pl1dfsgupstream/8.4pl1dfsg
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 c5969d17..444a7ee5 100644 --- a/Makefile.common +++ b/Makefile.common @@ -119,8 +119,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:=-boot -n 72 -sl -small DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex |