diff options
author | 2012-05-31 22:20:14 +0000 | |
---|---|---|
committer | 2012-05-31 22:20:14 +0000 | |
commit | b02100226bacc2ebed8dd69adcb5bd8e1df27087 (patch) | |
tree | 84fb8af67f097869e3d47e59d3358954a4062530 /tools | |
parent | 58962f43da831ecb27d25703d52962599ea8ed23 (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.ml | 2 |
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 |