aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqwc.mll
diff options
context:
space:
mode:
authorGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-25 14:31:15 +0200
committerGravatar Gaetan Gilbert <gaetan.gilbert@ens-lyon.fr>2017-04-27 21:42:01 +0200
commit87910d7be9bd50de4db80f70c6e287c7c7994460 (patch)
treeff0c9daa7ff73f0eb19e8b62ea6f689b154f314b /tools/coqwc.mll
parent5eb09af1e3686d6ac518b9eafe7cfcebd2b16375 (diff)
Fix 4.04 warnings
Diffstat (limited to 'tools/coqwc.mll')
-rw-r--r--tools/coqwc.mll2
1 files changed, 2 insertions, 0 deletions
diff --git a/tools/coqwc.mll b/tools/coqwc.mll
index b4fc738d0..cd07d4216 100644
--- a/tools/coqwc.mll
+++ b/tools/coqwc.mll
@@ -239,6 +239,7 @@ let process_channel ch =
if !skip_header then read_header lb;
spec lb
+[@@@ocaml.warning "-52"]
let process_file f =
try
let ch = open_in f in
@@ -251,6 +252,7 @@ let process_file f =
flush stdout; eprintf "coqwc: %s: Is a directory\n" f; flush stderr
| Sys_error s ->
flush stdout; eprintf "coqwc: %s\n" s; flush stderr
+[@@@ocaml.warning "+52"]
(*s Parsing of the command line. *)