aboutsummaryrefslogtreecommitdiff
path: root/tools/CoqMakefile.in
diff options
context:
space:
mode:
Diffstat (limited to 'tools/CoqMakefile.in')
-rw-r--r--tools/CoqMakefile.in2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/CoqMakefile.in b/tools/CoqMakefile.in
index 9097195721..0086516785 100644
--- a/tools/CoqMakefile.in
+++ b/tools/CoqMakefile.in
@@ -467,7 +467,7 @@ vok: $(VOFILES:%.vo=%.vok)
.PHONY: vok
validate: $(VOFILES)
- $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS) $^
+ $(TIMER) $(COQCHK) $(COQCHKFLAGS) $(COQLIBS_NOML) $^
.PHONY: validate
only: $(TGTS)