diff options
| author |  Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-11-06 18:49:21 +0100 |
|---|---|---|
| committer | Pierre Courtieu <Pierre.Courtieu@cnam.fr> | 2015-11-06 18:55:36 +0100 |
| commit | c5d380548ef5597b77c7ab1fce252704deefeaf1 (patch) | |
| tree | e4339d11ef650c9db43b851c9fd8736009306efa /tools/coqdep_boot.ml | |
| parent | a8b248096e5120f58157b0fc3bd06ca07118a8ab (diff) | |
Fixed #4407.
Like coqc: detect if the current directory was set by options, if not: add
it with empty logical path.
TODO: check if coq_makefile is still correct wrt to this modification, I
think yes, actually it should end being more correct.
Diffstat (limited to 'tools/coqdep_boot.ml')
| -rw-r--r-- | tools/coqdep_boot.ml | 12 |
1 files changed, 6 insertions, 6 deletions
diff --git a/tools/coqdep_boot.ml b/tools/coqdep_boot.ml index 64ce66d2d..088ea6bfc 100644 --- a/tools/coqdep_boot.ml +++ b/tools/coqdep_boot.ml @@ -35,15 +35,15 @@ let _ = if Array.length Sys.argv < 2 then exit 1; parse (List.tl (Array.to_list Sys.argv)); if !option_c then begin - add_rec_dir add_known "." []; - add_rec_dir (fun _ -> add_caml_known) "." ["Coq"]; + add_rec_dir_import add_known "." []; + add_rec_dir_import (fun _ -> add_caml_known) "." ["Coq"]; end else begin - add_rec_dir add_known "theories" ["Coq"]; - add_rec_dir add_known "plugins" ["Coq"]; + add_rec_dir_import add_known "theories" ["Coq"]; + add_rec_dir_import add_known "plugins" ["Coq"]; add_caml_dir "tactics"; - add_rec_dir (fun _ -> add_caml_known) "theories" ["Coq"]; - add_rec_dir (fun _ -> add_caml_known) "plugins" ["Coq"]; + add_rec_dir_import (fun _ -> add_caml_known) "theories" ["Coq"]; + add_rec_dir_import (fun _ -> add_caml_known) "plugins" ["Coq"]; end; if !option_c then mL_dependencies (); coq_dependencies () |