diff options
Diffstat (limited to 'Makefile.doc')
| -rw-r--r-- | Makefile.doc | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/Makefile.doc b/Makefile.doc index 39c3255f5..c31d81c8b 100644 --- a/Makefile.doc +++ b/Makefile.doc @@ -38,7 +38,11 @@ HEVEAOPTS:=-fix -exec xxdate.exe HEVEALIB:=/usr/local/lib/hevea:/usr/lib/hevea HTMLSTYLE:=simple export TEXINPUTS:=$(HEVEALIB): +ifdef COQDOC_NOBOOT +COQTEXOPTS:=-n 72 -sl -small +else COQTEXOPTS:=-boot -n 72 -sl -small +endif DOCCOMMON:=doc/common/version.tex doc/common/title.tex doc/common/macros.tex |