diff options
| author | herbelin | 2007-02-24 15:22:07 +0000 |
|---|---|---|
| committer | herbelin | 2007-02-24 15:22:07 +0000 |
| commit | f7a82d5f7edcce7ef70b99a10b92d8dcd5cfea70 (patch) | |
| tree | 7248e936a9094bff92ed96e666c8feb1941b5802 /library | |
| parent | 8eeec81e418603eaffc295bf20744da91b2e0f83 (diff) | |
Une passe sur les warnings (ajout Options.warn déclenchée par compile-verbose +
ajout Pp.strbrk pour faciliter les césures faciles + messages divers).
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@9679 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'library')
| -rw-r--r-- | library/library.ml | 10 |
1 files changed, 5 insertions, 5 deletions
diff --git a/library/library.ml b/library/library.ml index 7e93db65e4..70eac95aec 100644 --- a/library/library.ml +++ b/library/library.ml @@ -86,10 +86,10 @@ let add_load_path (phys_path,coq_path) = begin (* Assume the user is concerned by library naming *) if dir <> Nameops.default_root_prefix then - (Options.if_verbose warning (phys_path^" was previously bound to " - ^(string_of_dirpath dir) - ^("\nIt is remapped to "^(string_of_dirpath coq_path))); - flush_all ()); + Options.if_warn msg_warning + (str phys_path ++ strbrk " was previously bound to " ++ + pr_dirpath dir ++ strbrk "; it is remapped to " ++ + pr_dirpath coq_path); remove_load_path phys_path; load_paths := (phys_path::fst !load_paths, coq_path::snd !load_paths) end @@ -614,7 +614,7 @@ let save_library_to dir f = let di = Digest.file f' in System.marshal_out ch di; close_out ch - with e -> (warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e) + with e -> warning ("Removed file "^f'); close_out ch; Sys.remove f'; raise e (************************************************************************) (*s Display the memory use of a library. *) |