aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coqwc.mll
diff options
context:
space:
mode:
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. *)