diff options
| author |  Maxime Dénès <mail@maximedenes.fr> | 2017-10-03 12:11:50 +0200 |
|---|---|---|
| committer | Maxime Dénès <mail@maximedenes.fr> | 2017-10-03 12:11:50 +0200 |
| commit | 23ea4e3110fc4ec2da7d06ee009a1d30418e2493 (patch) | |
| tree | bcb0fb3dbf1d4e1386015cf8b6060905bdf56c2d /tools | |
| parent | c2c4a0566d5ec93f48de29dfdad2e4d3c1cec32d (diff) | |
| parent | 6f039e936d5039388d969d7bf0e1763f8f5c8397 (diff) | |
Merge PR #1076: 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) |