From ac72003e5f068b9cc7f521c45e497736ef4f0560 Mon Sep 17 00:00:00 2001
From: Enrico Tassi
Date: Thu, 10 Jan 2019 10:45:20 +0100
Subject: [make] support for QUICK

The variable QUICK enables the quick compilation chain:
- all v files are compiled with -quick to vio files (also
  -native-compiler no, since it is quicker)
- then all vio files are turned to vo files $NJOBS at a time

All occurrences of .vo use now .$(VO) that can be either
.vo or .vio depending of QUICK being defined. Targets that
only make sense for .vo files have to use $(VAR:.$(VO)=.vo)
---
 Makefile.doc | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.doc')

diff --git a/Makefile.doc b/Makefile.doc
index 9e6ec4955a..db60189870 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -137,7 +137,7 @@ else
 doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO)
 endif
 	$(COQDOC) -q -boot --gallina --body-only --latex --stdout \
-            -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@
+            -R theories Coq $(THEORIESLIGHTVO:.$(VO)=.v) >> $@
 
 doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex
 	(cd doc/stdlib;\
-- 
cgit v1.2.3