diff options
| author |  Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-05-27 16:00:53 +0200 |
|---|---|---|
| committer | Gaëtan Gilbert <gaetan.gilbert@ens-lyon.fr> | 2017-05-28 12:52:55 +0200 |
| commit | 149b0c422027a31972b62457af1bf97bd016e26c (patch) | |
| tree | 32f5267f4f24086018d1c04e71a236392f089993 /Makefile.doc | |
| parent | 2eb27e56ea4764fa2f2acec6f951eef2642ff1be (diff) | |
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 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 |