diff options
author | Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
---|---|---|
committer | Stephane Glondu <steph@glondu.net> | 2014-01-19 15:09:23 +0100 |
commit | d2c5c5e616a6e118291fe1ce9965c731adac03a8 (patch) | |
tree | 7b000ad50dcc45ff1c63768a983cded1e23a07ca /plugins/xml/cic2acic.ml | |
parent | db38bb4ad9aff74576d3b7f00028d48f0447d5bd (diff) |
Imported Upstream version 8.4pl3dfsgupstream/8.4pl3dfsg
Diffstat (limited to 'plugins/xml/cic2acic.ml')
-rw-r--r-- | plugins/xml/cic2acic.ml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/plugins/xml/cic2acic.ml b/plugins/xml/cic2acic.ml index a14eda60..165bf83d 100644 --- a/plugins/xml/cic2acic.ml +++ b/plugins/xml/cic2acic.ml @@ -23,7 +23,7 @@ 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 "^ + Pp.msg_warn ("Modules not supported: reference to "^ Libnames.string_of_path path^" will be wrong"); dirpath | [modul] -> modul |