diff --git a/src/shared/init.cpp b/src/shared/init.cpp index 3428b7dfbd..95c7f227c8 100644 --- a/src/shared/init.cpp +++ b/src/shared/init.cpp @@ -7,5 +7,5 @@ Author: Leonardo de Moura #include "init/init.h" namespace lean { // automatic initialization for the shared library -// initializer g_init; +initializer g_init; }