diff options
| author |  Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-09-21 18:32:56 +0200 |
|---|---|---|
| committer | Guillaume Melquiond <guillaume.melquiond@inria.fr> | 2017-09-21 18:32:56 +0200 |
| commit | 6f039e936d5039388d969d7bf0e1763f8f5c8397 (patch) | |
| tree | 64d1cb6babae37db6a4757c84ff2dea4f275d52e /tools | |
| parent | 9933871efd122163f7e2dfe8377b9b2dd384b47b (diff) | |
Properly handle "coq_makefile -Q . Foo" (bug #5580).
Diffstat (limited to 'tools')
| -rw-r--r-- | tools/coq_makefile.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index de76bf98b..4a9d871fd 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -274,7 +274,7 @@ let generate_conf oc project args = ;; let ensure_root_dir - ({ ml_includes; r_includes; + ({ ml_includes; r_includes; q_includes; v_files; ml_files; mli_files; ml4_files; mllib_files; mlpack_files } as project) = @@ -283,6 +283,7 @@ let ensure_root_dir let not_tops = List.for_all (fun s -> s <> Filename.basename s) in if exists (fun { canonical_path = x } -> x = here) ml_includes || exists (fun ({ canonical_path = x },_) -> is_prefix x here) r_includes + || exists (fun ({ canonical_path = x },_) -> is_prefix x here) q_includes || (not_tops v_files && not_tops mli_files && not_tops ml4_files && not_tops ml_files && not_tops mllib_files && not_tops mlpack_files) |