aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/aux_file.ml
diff options
context:
space:
mode:
authorGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-02-27 16:13:22 +0100
committerGravatar Enrico Tassi <Enrico.Tassi@inria.fr>2014-02-27 16:13:22 +0100
commitca64cc032a3f03381d00d7c9b128688f3f920844 (patch)
tree29f6e6fb077b82f1fcc6f11d3bd2e39adc9fe2f1 /lib/aux_file.ml
parent62852f6f2ab6d3abc53c4289cd46a52d1abd4a2d (diff)
amending last commit
Diffstat (limited to 'lib/aux_file.ml')
-rw-r--r--lib/aux_file.ml4
1 files changed, 2 insertions, 2 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml
index aceded526..5a3d29746 100644
--- a/lib/aux_file.ml
+++ b/lib/aux_file.ml
@@ -79,6 +79,6 @@ let load_aux_file_for vfile =
| Outdated -> empty_aux_file
| Sys_error s | Scanf.Scan_failure s
| Failure s | Invalid_argument s ->
- Flage.if_verbose
- Pp.(msg_warning (str"Loading file "++str aux_fname++str": "++str s));
+ Flags.if_verbose
+ Pp.msg_warning Pp.(str"Loading file "++str aux_fname++str": "++str s);
empty_aux_file