From f76c5bbde96d27414bc7c389d322d868d01b393e Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 18 Oct 2014 09:01:24 -0700 Subject: [PATCH] fix(init): initialization problem --- src/init/init.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/init/init.cpp b/src/init/init.cpp index de96a4a75..214dc5563 100644 --- a/src/init/init.cpp +++ b/src/init/init.cpp @@ -26,10 +26,10 @@ void initialize() { initialize_sexpr_module(); initialize_kernel_module(); initialize_inductive_module(); + init_default_print_fn(); initialize_library_module(); initialize_tactic_module(); initialize_frontend_lean_module(); - init_default_print_fn(); register_modules(); } void finalize() {