diff options
| author |  Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-27 15:17:04 +0100 |
|---|---|---|
| committer | Enrico Tassi <Enrico.Tassi@inria.fr> | 2014-02-27 15:52:40 +0100 |
| commit | 62852f6f2ab6d3abc53c4289cd46a52d1abd4a2d (patch) | |
| tree | 94ccbac88b885a64966252ba21af63367e252396 /lib | |
| parent | edd06dfa60a3535b93da92bdc0f26e412c3e2d6c (diff) | |
better warning
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/aux_file.ml | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/lib/aux_file.ml b/lib/aux_file.ml index 98f1a51b8..aceded526 100644 --- a/lib/aux_file.ml +++ b/lib/aux_file.ml @@ -79,5 +79,6 @@ let load_aux_file_for vfile = | Outdated -> empty_aux_file | Sys_error s | Scanf.Scan_failure s | Failure s | Invalid_argument s -> - Pp.(msg_error (str"Error loading file "++str aux_fname++str" : "++str s)); + Flage.if_verbose + Pp.(msg_warning (str"Loading file "++str aux_fname++str": "++str s)); empty_aux_file |