aboutsummaryrefslogtreecommitdiff
path: root/Makefile.build
diff options
context:
space:
mode:
authorPierre-Marie Pédrot2018-11-07 11:42:38 +0100
committerPierre-Marie Pédrot2018-11-07 11:42:38 +0100
commit19b7ce2f39eaf37e48d1d12ef73defab3c9fbdb2 (patch)
treea55af313e25a17382c94a60805b95e82f02ef6c6 /Makefile.build
parente857efb2e61c29a5b0b29702ca8d746ea2580ca6 (diff)
parent7f2946157797ba7da3ed8712c10f5a0302b36d49 (diff)
Merge PR #8773: [checker] Refactor by sharing code with the kernel
Diffstat (limited to 'Makefile.build')
-rw-r--r--Makefile.build2
1 files changed, 1 insertions, 1 deletions
diff --git a/Makefile.build b/Makefile.build
index fb84a131c7..ee856aae8e 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -612,7 +612,7 @@ VALIDOPTS=$(if $(VERBOSE),,-silent) -o -m
validate: $(CHICKEN) | $(ALLVO)
$(SHOW)'COQCHK <theories & plugins>'
- $(HIDE)$(CHICKEN) -boot $(VALIDOPTS) $(ALLMODS)
+ $(HIDE)$(CHICKEN) -boot -debug $(VALIDOPTS) $(ALLMODS)
$(ALLSTDLIB).v:
$(SHOW)'MAKE $(notdir $@)'