From a4218c4313adbe841c7cd7dda4eddf8a6f8e8dd6 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Mon, 5 Dec 2016 16:48:29 -0800 Subject: [PATCH] fix(shared/init): shared library initialization --- src/shared/init.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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; }