aboutsummaryrefslogtreecommitdiffhomepage
path: root/plugins/xml/cic2acic.ml
diff options
context:
space:
mode:
authorGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-30 16:05:13 +0000
committerGravatar ppedrot <ppedrot@85f007b7-540e-0410-9357-904b9bb8a0f7>2012-05-30 16:05:13 +0000
commit24879dc0e59856e297b0172d00d67df67fbb0184 (patch)
treed57ffef43297aa7f8b29830f3bde7f3bd334babb /plugins/xml/cic2acic.ml
parentf9d97c62b2e46829a6ece74d07f5fab2cea1d769 (diff)
More uniformisation in Pp.warn functions.
git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15399 85f007b7-540e-0410-9357-904b9bb8a0f7
Diffstat (limited to 'plugins/xml/cic2acic.ml')
-rw-r--r--plugins/xml/cic2acic.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml
index ec0910d7f..e29fcd0e8 100644
--- a/plugins/xml/cic2acic.ml
+++ b/plugins/xml/cic2acic.ml
@@ -23,8 +23,8 @@ let get_module_path_of_full_path path =
(function modul -> Libnames.is_dirpath_prefix_of modul dirpath) modules
with
[] ->
- Pp.warning ("Modules not supported: reference to "^
- Libnames.string_of_path path^" will be wrong");
+ Pp.msg_warning (Pp.str ("Modules not supported: reference to "^
+ Libnames.string_of_path path^" will be wrong"));
dirpath
| [modul] -> modul
| _ ->