From 797eb524853e361f84c9c776024c142107f0c282 Mon Sep 17 00:00:00 2001
From: charguer
Date: Thu, 12 Dec 2019 10:48:50 +0100
Subject: Fix #11195 and add other improvements: try loading .vio (and not just
 .vo) if the .vos file is empty, rename -quick to -vio, dump empty .vos when
 producing .vio, dump empty .vos and .vok files when producing .vo from .vio.

---
 Makefile.build | 6 +++---
 1 file changed, 3 insertions(+), 3 deletions(-)

(limited to 'Makefile.build')

diff --git a/Makefile.build b/Makefile.build
index 5b879220d0..a8ae040f8e 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -840,7 +840,7 @@ theories/Init/%.vo theories/Init/%.glob: theories/Init/%.v $(VO_TOOLS_DEP)
 
 theories/Init/%.vio: theories/Init/%.v $(VO_TOOLS_DEP)
 	$(SHOW)'COQC -quick -noinit $<'
-	$(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq -quick -noglob
+	$(HIDE)$(BOOTCOQC) $< -noinit -R theories Coq -vio -noglob
 
 # The general rule for building .vo files :
 
@@ -855,8 +855,8 @@ ifdef VALIDATE
 endif
 
 %.vio: %.v theories/Init/Prelude.vio $(VO_TOOLS_DEP)
-	$(SHOW)'COQC -quick $<'
-	$(HIDE)$(BOOTCOQC) $< -quick -noglob
+	$(SHOW)'COQC -vio $<'
+	$(HIDE)$(BOOTCOQC) $< -vio -noglob
 
 %.v.timing.diff: %.v.before-timing %.v.after-timing
 	$(SHOW)PYTHON TIMING-DIFF $<
-- 
cgit v1.2.3