From 8dc97f734f90f50980b636e2c0c8de34d20a5843 Mon Sep 17 00:00:00 2001
From: Ralf Jung <post@ralfj.de>
Date: Wed, 20 Sep 2017 12:59:38 +0200
Subject: new quick2vo target: like vio2vo, but smarter

---
 tools/CoqMakefile.in | 14 +++++++++++++-
 1 file changed, 13 insertions(+), 1 deletion(-)

(limited to 'tools')

diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index ca02c983d..a426c3cb2 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -381,7 +381,7 @@ bytefiles: $(CMOFILES) $(CMAFILES)
 optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES))
 .PHONY: optfiles
 
-# FIXME, see Ralph's bugreport
+# FIXME, see Ralf's bugreport
 quick: $(VOFILES:.vo=.vio)
 .PHONY: quick
 
@@ -390,6 +390,18 @@ vio2vo:
 		-schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio)
 .PHONY: vio2vo
 
+quick2vo:
+	$(HIDE)make -j $(J) quick
+	$(HIDE)VIOFILES=$$(for vofile in $(VOFILES); do \
+	  viofile="$$(echo "$$vofile" | sed "s/\.vo$$/.vio/")"; \
+	  if [ "$$vofile" -ot "$$viofile" -o ! -e "$$vofile" ]; then printf "$$viofile "; fi; \
+	done); \
+	echo "VIO2VO: $$VIOFILES"; \
+	if [ -n "$$VIOFILES" ]; then \
+	  $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) -schedule-vio2vo $(J) $$VIOFILES; \
+	fi
+.PHONY: quick2vo
+
 checkproofs:
 	$(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) \
 		-schedule-vio-checking $(J) $(VOFILES:%.vo=%.vio)
-- 
cgit v1.2.3