max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

fix(shell/lean): disable initialize/finalize server when -DSERVER=OFF is used

Browse source
This commit is contained in:
Leonardo de Moura 2016-10-14 12:56:50 -07:00
parent 39dba8f5e5
commit 541e9010e1
1 changed files with 4 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/shell/lean.cpp
View file

@ -224,10 +224,14 @@ private:
lean::initializer m_init;
public:
initializer() {
#if defined(LEAN_SERVER)
lean::initialize_server();
#endif
}
~initializer() {
#if defined(LEAN_SERVER)
lean::finalize_server();
#endif
}
};