aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools
diff options
context:
space:
mode:
authorGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-31 22:20:14 +0000
committerGravatar pboutill <pboutill@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-31 22:20:14 +0000
commitb02100226bacc2ebed8dd69adcb5bd8e1df27087 (patch)
tree84fb8af67f097869e3d47e59d3358954a4062530 /tools
parent58962f43da831ecb27d25703d52962599ea8ed23 (diff)
Coq_makefile bug for plugins
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15405 85f007b7-540e-0410-9357-904b9bb8a0f7
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