diff options
| author | charguer | 2019-12-12 10:48:50 +0100 |
|---|---|---|
| committer | charguer | 2019-12-12 13:57:18 +0100 |
| commit | 797eb524853e361f84c9c776024c142107f0c282 (patch) | |
| tree | 410a97bd2904fc790a6191cddb18de76ce77791f /tools | |
| parent | 4a7a5c36802701d0e1b47956bb14cfc9cab99baa (diff) | |
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.
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/CoqMakefile.in | 13 |
1 files changed, 9 insertions, 4 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in index 7c53ecfe18..600494625b 100644 --- a/tools/CoqMakefile.in +++ b/tools/CoqMakefile.in @@ -389,7 +389,11 @@ optfiles: $(if $(DO_NATDYNLINK),$(CMXSFILES)) .PHONY: optfiles # FIXME, see Ralf's bugreport -quick: $(VOFILES:.vo=.vio) +# quick is deprecated, now renamed vio +vio: $(VOFILES:.vo=.vio) +.PHONY: vio +quick: vio + $(warning "'make quick' is deprecated, use 'make vio' or consider using 'vos' files") .PHONY: quick vio2vo: @@ -397,8 +401,9 @@ vio2vo: -schedule-vio2vo $(J) $(VOFILES:%.vo=%.vio) .PHONY: vio2vo +# quick2vo is undocumented quick2vo: - $(HIDE)make -j $(J) quick + $(HIDE)make -j $(J) vio $(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; \ @@ -677,8 +682,8 @@ $(GLOBFILES): %.glob: %.v $(TIMER) $(COQC) $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< $(VFILES:.v=.vio): %.vio: %.v - $(SHOW)COQC -quick $< - $(HIDE)$(TIMER) $(COQC) -quick $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< + $(SHOW)COQC -vio $< + $(HIDE)$(TIMER) $(COQC) -vio $(COQDEBUG) $(COQFLAGS) $(COQLIBS) $< $(VFILES:.v=.vos): %.vos: %.v $(SHOW)COQC -vos $< |