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 /Makefile.build | |
| 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 'Makefile.build')
| -rw-r--r-- | Makefile.build | 6 |
1 files changed, 3 insertions, 3 deletions
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 $< |