diff options
Diffstat (limited to 'tools/coq_makefile.ml')
| -rw-r--r-- | tools/coq_makefile.ml | 4 |
1 files changed, 1 insertions, 3 deletions
diff --git a/tools/coq_makefile.ml b/tools/coq_makefile.ml index 954c21d58..e902370c3 100644 --- a/tools/coq_makefile.ml +++ b/tools/coq_makefile.ml @@ -843,11 +843,9 @@ let do_makefile args = if not (makefile = None) then close_out !output_channel; exit 0 -let main () = +let _ = let args = if Array.length Sys.argv = 1 then usage (); List.tl (Array.to_list Sys.argv) in do_makefile args - -let _ = Printexc.catch main () |