diff options
Diffstat (limited to 'Makefile.build')
| -rw-r--r-- | Makefile.build | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build index 661e762dea..d8b9df0d42 100644 --- a/Makefile.build +++ b/Makefile.build @@ -370,7 +370,8 @@ install-ide-info: .PHONY: validate check test-suite $(ALLSTDLIB).v -VALIDOPTS=-silent -o -m + +VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m validate:: $(CHICKEN) $(ALLVO) $(SHOW)'COQCHK <theories & plugins>' |