aboutsummaryrefslogtreecommitdiff
path: root/tools/coqwc.mll
diff options
context:
space:
mode:
authorMaxime Dénès2017-05-02 16:04:50 +0200
committerMaxime Dénès2017-05-02 16:04:50 +0200
commit28accc370aa2f6fafbf50b69be7ae5dc06104212 (patch)
tree7764de5a598390e9906f064170a480cfcfe0a38d /tools/coqwc.mll
parent63503b99c46b27009e85e5c0fa9588b7424a589d (diff)
parent9a48211ea8439a8502145e508b70ede9b5929b2f (diff)
Merge PR#582: Fix 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 b4fc738d0e..cd07d4216f 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. *)