From 6f039e936d5039388d969d7bf0e1763f8f5c8397 Mon Sep 17 00:00:00 2001 From: Guillaume Melquiond Date: Thu, 21 Sep 2017 18:32:56 +0200 Subject: Properly handle "coq_makefile -Q . Foo" (bug #5580). --- tools/coq_makefile.ml | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'tools') 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) -- cgit v1.2.3