aboutsummaryrefslogtreecommitdiffhomepage
path: root/tools/coq_tex.ml
diff options
context:
space:
mode:
authorGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-07-30 07:56:49 +0200
committerGravatar Guillaume Melquiond <guillaume.melquiond@inria.fr>2015-07-30 07:56:49 +0200
commit5383cdc276d9ba7f1bb05bfe5aeae0a25edbd4a4 (patch)
tree314bbbcdf4b932bf98de14c19831ac4e5cfc8ee5 /tools/coq_tex.ml
parent9a5fb78ef3c7c5d4f568a4d04e169475e9105def (diff)
Remove usage of Printexc.catch in the tools, as it is deprecated since 2001.
"This function is deprecated: the runtime system is now able to print uncaught exceptions as precisely as Printexc.catch does. Moreover, calling Printexc.catch makes it harder to track the location of the exception using the debugger or the stack backtrace facility. So, do not use Printexc.catch in new code."
Diffstat (limited to 'tools/coq_tex.ml')
-rw-r--r--tools/coq_tex.ml4
1 files changed, 1 insertions, 3 deletions
diff --git a/tools/coq_tex.ml b/tools/coq_tex.ml
index f65708698..53444cee7 100644
--- a/tools/coq_tex.ml
+++ b/tools/coq_tex.ml
@@ -285,7 +285,7 @@ let find_coqtop () =
"coqtop"
end
-let main () =
+let _ =
parse_cl ();
if !image = "" then image := Filename.quote (find_coqtop ());
if !boot then image := !image ^ " -boot";
@@ -298,5 +298,3 @@ let main () =
flush stdout
end;
List.iter one_file (List.rev !files)
-
-let _ = Printexc.catch main ()