diff options
Diffstat (limited to 'library/loadpath.ml')
| -rw-r--r-- | library/loadpath.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/library/loadpath.ml b/library/loadpath.ml index 873703aff..60799a8a7 100644 --- a/library/loadpath.ml +++ b/library/loadpath.ml @@ -74,7 +74,7 @@ let add_load_path phys_path isroot coq_path = begin (* Assume the user is concerned by library naming *) if not (DirPath.equal dir Nameops.default_root_prefix) then - Flags.if_warn msg_warning + msg_warning (str phys_path ++ strbrk " was previously bound to " ++ pr_dirpath dir ++ strbrk "; it is remapped to " ++ pr_dirpath coq_path); |