diff options
| author | Emilio Jesus Gallego Arias | 2019-02-22 11:52:30 +0100 |
|---|---|---|
| committer | Emilio Jesus Gallego Arias | 2019-02-22 11:52:30 +0100 |
| commit | fa3a97426013cf940cd25abde43c0191766218b1 (patch) | |
| tree | 9a007accd6feef4a852610dbc6095f5e5d68cd59 /Makefile.build | |
| parent | 5f7bb95b6532a6983a2d1880aa531e4e4dd6568d (diff) | |
| parent | 2abf8037772ee1bb9fbfa255800222663daf18e5 (diff) | |
Merge PR #9614: Fix #9613 use -coqlib when invoking coqchk
Reviewed-by: ejgallego
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 8afb498a63..2b401cd9e6 100644 --- a/Makefile.build +++ b/Makefile.build @@ -550,11 +550,11 @@ $(CSDPCERTBYTE): $(CSDPCERTCMO) .PHONY: validate check test-suite $(ALLSTDLIB).v -VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m +VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m -coqlib . validate: $(CHICKEN) | $(ALLVO:.$(VO)=.vo) $(SHOW)'COQCHK <theories & plugins>' - $(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS) + $(HIDE)$(CHICKEN) $(VALIDOPTS) $(ALLMODS) $(ALLSTDLIB).v: $(SHOW)'MAKE $(notdir $@)' @@ -828,7 +828,7 @@ theories/Init/%.vio: theories/Init/%.v $(VO_TOOLS_DEP) $(HIDE)$(BOOTCOQC) $< $(TIMING_ARG) $(TIMING_EXTRA) ifdef VALIDATE $(SHOW)'COQCHK $(call vo_to_mod,$@)' - $(HIDE)$(CHICKEN) -boot -silent -norec $(call vo_to_mod,$@) \ + $(HIDE)$(CHICKEN) $(VALIDOPTS) -norec $(call vo_to_mod,$@) \ || ( RV=$$?; rm -f "$@"; exit $${RV} ) endif |