From 149b0c422027a31972b62457af1bf97bd016e26c Mon Sep 17 00:00:00 2001 From: Gaëtan Gilbert Date: Sat, 27 May 2017 16:00:53 +0200 Subject: Gitlab CI --- Makefile.doc | 4 ++++ 1 file changed, 4 insertions(+) (limited to 'Makefile.doc') 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 -- cgit v1.2.3