michael/lean2
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions

fix(style): remove "using namespace emscripten"

Browse source
This commit is contained in:
Soonho Kong 2014-10-14 21:09:33 -07:00
parent 4143716311
commit 9a6e18ad2a
1 changed files with 3 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/shell/lean.cpp
View file

@ -236,7 +236,6 @@ environment import_standard(environment const & env, io_state const & ios, bool
#if defined(LEAN_EMSCRIPTEN)
#include <emscripten/bind.h>
using namespace emscripten;
class emscripten_shell {
private:
@ -299,9 +298,9 @@ int emscripten_process_file(std::string input_filename) {
}
EMSCRIPTEN_BINDINGS(LEAN_JS) {
function("lean_init", &emscripten_init);
function("lean_import_module", &emscripten_import_module);
function("lean_process_file", &emscripten_process_file);
emscripten::function("lean_init", &emscripten_init);
emscripten::function("lean_import_module", &emscripten_import_module);
emscripten::function("lean_process_file", &emscripten_process_file);
}
int main() {