Formerly main.c.~100~

diff --git a/main.c b/main.c
index 4e8251e1e407b68ef2d641825896be3c4a514659..dd06aa4730e3eb9ed88cba90c98f2f6f8a04cfd5 100644 (file)
--- a/main.c
+++ b/main.c
@@ -396,8 +396,6 @@ main (argc, argv, envp)
   PATH_VAR (current_directory);
   char *directory_before_chdir;
 
-mcheck(0);
-
   default_goal_file = 0;
   reading_filename = 0;
   reading_lineno_ptr = 0;