diff options
Diffstat (limited to 'library/loadpath.ml')
| -rw-r--r-- | library/loadpath.ml | 18 |
1 files changed, 10 insertions, 8 deletions
diff --git a/library/loadpath.ml b/library/loadpath.ml index f8169576dd..d03c6c5553 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -8,7 +8,7 @@ open Pp open Util -open Errors +open CErrors open Names open Libnames @@ -50,6 +50,13 @@ let remove_load_path dir = let filter p = not (String.equal p.path_physical dir) in load_paths := List.filter filter !load_paths +let warn_overriding_logical_loadpath = + CWarnings.create ~name:"overriding-logical-loadpath" ~category:"loadpath" + (fun (phys_path, old_path, coq_path) -> + str phys_path ++ strbrk " was previously bound to " ++ + pr_dirpath old_path ++ strbrk "; it is remapped to " ++ + pr_dirpath coq_path) + let add_load_path phys_path coq_path ~implicit = let phys_path = CUnix.canonical_path_name phys_path in let filter p = String.equal p.path_physical phys_path in @@ -65,17 +72,12 @@ let add_load_path phys_path coq_path ~implicit = let replace = if DirPath.equal coq_path old_path then implicit <> old_implicit - else if DirPath.equal coq_path (Nameops.default_root_prefix) - && String.equal phys_path (CUnix.canonical_path_name Filename.current_dir_name) then - false (* This is the default "-I ." path, don't override the old path *) else let () = (* Do not warn when overriding the default "-I ." path *) if not (DirPath.equal old_path Nameops.default_root_prefix) then - msg_warning - (str phys_path ++ strbrk " was previously bound to " ++ - pr_dirpath old_path ++ strbrk "; it is remapped to " ++ - pr_dirpath coq_path) in + warn_overriding_logical_loadpath (phys_path, old_path, coq_path) + in true in if replace then begin |