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

(limited to 'Makefile.ide')

diff --git a/Makefile.ide b/Makefile.ide
index cae77ee348..23ce83d263 100644
--- a/Makefile.ide
+++ b/Makefile.ide
@@ -70,7 +70,7 @@ SOURCEVIEWSHARE=$(shell pkg-config --variable=prefix gtksourceview-2.0)/share
 .PHONY: ide-toploop ide-byteloop ide-optloop
 
 # target to build CoqIde (native version) and the stuff needed to lauch it
-coqide: coqide-files coqide-opt theories/Init/Prelude.vo
+coqide: coqide-files coqide-opt theories/Init/Prelude.$(VO)
 
 # target to build CoqIde (in native and byte versions), and no more
 # NB: this target is used in the opam package coq-coqide
-- 
cgit v1.2.3