diff options
| author | Maxime Dénès | 2017-05-29 23:26:23 +0200 |
|---|---|---|
| committer | Maxime Dénès | 2017-05-29 23:26:23 +0200 |
| commit | 0336d4d19d446315cb922149b8ee4e7885843be0 (patch) | |
| tree | 736e7d580a255d2438a5514ea37b609560bb40a3 /Makefile.doc | |
| parent | 42c752cf0336cbadc8e9c092ff5aed6a38899dda (diff) | |
| parent | 149b0c422027a31972b62457af1bf97bd016e26c (diff) | |
Merge PR#687: Gitlab CI
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 39c3255f5c..c31d81c8bc 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 |