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.dev | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

(limited to 'Makefile.dev')

diff --git a/Makefile.dev b/Makefile.dev
index 9659f602d7..13b85dfad4 100644
--- a/Makefile.dev
+++ b/Makefile.dev
@@ -63,7 +63,7 @@ revision:
 
 coqlight: theories-light tools coqbinaries
 
-states: theories/Init/Prelude.vo
+states: theories/Init/Prelude.$(VO)
 
 miniopt: $(COQTOPEXE) pluginsopt
 minibyte: $(COQTOPBYTE) pluginsbyte
-- 
cgit v1.2.3