aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
Diffstat (limited to 'tools')
-rw-r--r--tools/coq_makefile.ml2
1 files changed, 1 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml
index f38eed4c7..9d796f95c 100644
--- a/tools/coq_makefile.ml
+++ b/tools/coq_makefile.ml
@@ -429,7 +429,7 @@ let include_dirs (inc_i,inc_r) =
if !some_ml4file || !some_mlfile || !some_mlifile then begin
print "OCAMLLIBS?="; print_list "\\\n " str_i; print "\n";
end;
- if !some_vfile then begin
+ if !some_vfile || !some_mllibfile || !some_mlpackfile then begin
print "COQLIBS?="; print_list "\\\n " str_i'; print " "; print_list "\\\n " str_r; print "\n";
print "COQDOCLIBS?="; print_list "\\\n " str_r; print "\n\n";
end